Pascal André

Gilles Ardourel

Christian Attiogbé

A Formal Analysis Toolbox for the Kmelia Component Model

Keywords: Property Verification Toolbox, Components, Services, Model Checking

We present in this paper the COSTO toolbox that supports the Kmelia abstract component model. First, an overview of the COSTO toolbox is given. Then the abstract component model Kmelia is presented. One main feature of the toolbox is the connection with existing tools in order to perform the analysis of specification properties. We present this approach for the dynamic aspect analysis; an example of the connection with the CADP toolbox to check Kmelia service behavioural compatibility is used as an illustration.

Introduction

It is an important challenge to deliver correct software components on demand, from various development frameworks and for various problem requirements. Some identified parameters for the success of such enterprise are the availability of reliable, proof-certified and interoperable components. This is tightly related with the availability of tools to help in the design, development and analysis of the components.

Component Based Software Engineering emphasises the development of components and their assemblies to build large scale software. However, in practice the existing component model proposals, both in industry and academia, do not propose provably-correct components and they are quite different and even not interoperable. This motivates our work. For instance a given abstract component model, proved to have desired properties, may be refined into code with respect to various executable platforms. The obtained codes may be used in various software.

This work contributes to assist the user, with a toolbox, in the development of correct components and assemblies from their abstract specifications. Correctness is considered from various points of view: in this article we deal with the behavioural interaction between components.

In the article we present the Component Study Toolbox (COSTO) which is designed to support the Kmelia abstract component model. The toolbox is currently an experimental prototype not yet publicly available. We give an overview of the modules that compose the toolbox. Instead of presenting in details all the modules we focus on the ones concerned by the verification of dynamic properties and especially the LOTOS Module. It illustrates an important principle in COSTO: the use of adequate languages and tools to perform verifications.

The article is organised as follows. In Section 2 we give an overview of COSTO, our formal analysis toolbox for components. We present the Kmelia abstract component model based on services in Section 3; this model serves as the component model for property verification. Section 4 is devoted to the analysis of one property related to the dynamic aspect of components: behavioural compatibility. We present the principle of connecting the COSTO toolbox with existing tools by translating Kmelia specifications into targeted formalisms. In Section 5 we illustrate one component of the toolbox: the connection with CADP to check behavioural compatibility. Finally some perspectives are given in Section 6.

An Overview of the COSTO Toolbox

Considering that mechanisation is a means to assess design and development techniques based on formal methods, we start the development of a prototype named COSTO to support design and analysis of component using the Kmelia Abstract component model. The Kmelia abstract component model and the specification language named Kmelia are briefly described in Section 3.

One of the main features of COSTO is the definition of bridges to existing formal analysis frameworks and their integration in a verification process.

COSTO Main Modules

The COSTO prototype is composed of several modules written in Java. Most of them can be used in command-line, through their API or using the COSTO Eclipse plugins. Figure 1 shows the main COSTO modules. The Core module is the main COSTO module used by all the other modules. It contains a parser for Kmelia textual specifications based on ANTLR, and an API for manipulating the resulting Kmelia Object Models. Syntax analysis and basic typing checks are done during and after parsing.

The Verification module contains a verification framework that is used to define verification processes, execute them on Kmelia Object Models and manipulate verification results. Architectural properties analysis such as the correct composition of components according to their service signatures and interfaces are defined using this framework.

Consistency checks such as Component Interface consistency, Service consistency and Consistency between Services Interfaces and Behaviours rely on an earlier version of this module and they are currently being integrated in the verification framework to add more flexibility.

The LOTOS Analysis module contains a translator of Kmelia specifications to LOTOS specifications according to a context (this module is described in section 5). The generated LOTOS specifications can then be checked with CADP (a toolbox with various analysis modules, [START_REF] Garavel | An overview of cadp[END_REF]).

The MEC Analysis module contains an extractor which selects and transforms parts of a Kmelia behaviour specification into MEC specifications according to a context. It also generates properties to be checked with the MEC model checker. It features a MEC feedback analyser which parses MEC results and generates documentation in order to correct the Kmelia specification. In order to go beyond simple documentation, an automatic integration of this MEC feedback in the verification framework is under development.

The Export module contains generators that help in the documentation of the Kmelia specification. This module generates Kmelia component L A T E X documentation where service behaviours are exported into dot for graphical representation.

COSTO Eclipse Modules

In order to simplify the use of COSTO, several tools have been integrated to the Eclipse Integrated Development Environment as plugins.

Fig. 2. Using Eclipse plugins to verify Kmelia components

The previously described COSTO modules (see Figure 1) are packed into the coloss.costolib.base plugin. Several tools have been built in the coloss.costolib.ui:

• A text editor for Kmelia specifications which shows results from syntactic and consistency verifications;

• A tree-based view that outlines a Kmelia specification;

• Wizards for creating Kmelia components and assemblies;

• Menu actions for exporting a Kmelia specification to the various formats supported in the COSTO Exports module (such as L A T E X);

• Wizards for creating verification contexts and starting the verifications with MEC or LOTOS.

Figure 2 illustrates a scenario of use of the COSTO plugins: starting with a Kmelia specification, generated by a wizard or created with the editor, the user selects or creates a verification process and its context with a wizard, then he runs the verification that may or may not rely on an external tool, and finally he gets the verification result. The Kmelia examples from the following section have been generated or checked with the COSTO prototype.

A Multi-Service Component Model: Kmelia

We present here the specification language Kmelia which is central to the COSTO tool. Instead of presenting the language itself (syntax and semantics) we sketch a quick overview of its concepts using examples.

Kmelia is an abstract formal component model based on services [START_REF] Attiogbé | Checking Component Composability[END_REF][START_REF] André | Defining Component Protocols with Service Composition: Illustration withe Kmelia Model[END_REF]. Its goal is to describe component systems and to study their properties before any implementation. The interactions between components are described through services and synchronous communications. The dynamic behaviour of services is formally specified by labelled transition systems.

Related component models with dynamic behaviours (or protocols) are SOFA [START_REF] Plasil | Behavior protocols for software components[END_REF], Fractal [START_REF] Bruneton | The fractal component model and its support in java: Experiences with auto-adaptive and reconfigurable systems[END_REF], Tracta [START_REF] Giannakopoulou | Behaviour Analysis of Distributed Systems Using the Tracta Approach[END_REF], Wright [START_REF] Allen | A Formal Basis for Architectural Connection[END_REF] and others [START_REF] Yellin | Protocol Specifications and Component Adaptors[END_REF][START_REF] Attie | Correctness of Model-based Component Composition without State Explosion[END_REF][START_REF] Canal | Adding Roles to CORBA Objects[END_REF][START_REF] Pavel | Java Implementation of a Component Model with Explicit Symbolic Protocols[END_REF]. The main difference between Kmelia and the above models and proposals is that Kmelia emphasises the concept of service: (i) components are linked by their services rather than connected by structural ports or gates; (ii) dynamic behaviours are associated to services rather than to components2 ; (iii) services are functionalities that define contracts; (iv) services can be composed horizontally and vertically.

Components, Services and Assemblies

A Kmelia abstract component is a mathematical model of an open multi-service system that supports synchronous communication with its environment. A Kmelia component is defined through an abstract state model (made up with variables, an invariant, and an initialisation), an interface (made up with provided and required services) and a constraint definition (logic expressions). Yet, the property language is an ad hoc typed first order logic; the planned evolution is a language suitable to interact with existing theorem provers to check the expressions.

Let us illustrate the model with a simplified real-world problem: a bank Automatic Teller Machine (ATM). Since the case is very common, the details are omitted here. The ATM provides bank services (withdrawal, money deposit, query accounts...) to users. Figure 3 is a textual Kmelia specification of an ATM core component. The component interface provides four usual bank services for exchanging money and requires an external authorisation. The component state model manages the ATM cash data.

Basically, a Kmelia service encodes a functionality; it is defined with an interface and a behaviour. The service interface includes the service signature, the local declarations, the assertions (pre/post conditions) and the service dependency (i.e the list of services this service depends on). The service dependency of a service s i includes the references to provided subservices (they are the services which are provided in the context of another service) and to required services (those required in the context of s i ). The latter are required from the component itself, from the calling component or from any components. Figure 4 shows a specification of the withdrawal service of the core component for the ATM system in Kmelia. The subprovides, calrequires, extrequires clauses in the interface of the withdrawal service make explicit the hierarchy and the dependencies between services: the withdrawal service provides an ident subservice and requires three other services, two of them being required from the component which is calling withdrawal.

Component assemblies establish the communication channel used by the service communication actions. Assembling Kmelia components consists in linking their pairwise services: required services may be linked to provided services. An implicit channel is associated to this link that supports the communication actions or messages between the services (see section 3.2). The semantics of the links is not straightforward because it must conform to the service interface hierarchy. Indeed the services that appear in the subprovides and the calrequires clauses of the service interface dependency must (i) share a common link (they are sublinks) and (ii) their links must conform to the hierarchy levels. This constraint is recursive on service inclusion. A component composition is the encapsulation of an assembly within a component with a projection of services by promotion links. Promotion links relate the composite services to the inner component services.

Figure 5 is a graphical view of a Kmelia model for the bank ATM. The as com- ponent is a composition of an ATM CORE (ac) with an ATM user interface (ui). The main provided service behaviour of the ui component drives the user commands. For example, the user can ask for money (required service ask for money) which is linked to the service withdrawal provided by the ATM core ac component. According to Figure 5, the withdrawal service may call internal services (debit,...), external services (ask authorization), external services required from the caller (ask code, ask amount) and it provides the ident service in the context of ask code. Note that the amount and code links are sublinks: they share the ask for money-withdrawal link and its implicit communication channel. The assembly links support the interactions specified in the service behaviours.

Service Behaviour Description

In Kmelia, a service behaviour is an extended labelled transition system (eLTS) where the states define the service evolution steps and the transitions are labelled with possibly guarded combination of actions: [guard] action*. The actions are either elementary actions or communication actions. An elementary action (e.g. an assignment) does not involve other services; it does not use a communication channel. A communication action is either a service call/response or a message send/ receive.

The services run concurrently; the communications are synchronous. The communication actions use either the standard communication primitives ! and ? for sending/receiving simple messages or their extended forms !! and ?? to deal with service calls and service responses. They are prefixed with a communication channel which can either denote the required service ( service-name) or the caller ( CALLER) or the component itself ( SELF). A communication channel that is used in a service behaviour has to be established by a link. For example the ask for money-withdrawal link (Figure 5) establishes the caller service of the withdrawal service: CALLER = ask for money.

Figure 6 is a visual representation of the withdrawal service eLTS. This figure has been produced with the COSTO toolbox. A withdrawal consists in reading the given cash card. The user enters the password. The given password is compared with the card password. If the verification succeeds, the card holder is authenticated otherwise the password is requested again. When the verification fails three times, the card is swallowed. After the card holder identification in the withdrawal service, an authorisation is required from its ACD/ATM controller (AAC), which represents the bank management.

If the AAC accepts the transaction, the withdrawal service asks for the amount of cash, otherwise the card is ejected and the transaction ends. The user enters an amount which is compared with the current card policy limit. If the allowed amount is lower than the requested or if the current cash is not sufficient, the amount of cash is asked again. Otherwise, the transaction proceeds. In any positive case the withdrawal transaction ends after a card ejection.

In Kmelia, service behaviours may contain execution points (states or transitions) where a subservice (declared in the service's interface) can be called. These states or transitions are annotated with Kmelia's vertical structuring operators. For instance, the label of node e1 in Figure 6 means that the ident optional service may be called by a widthdrawal's caller when the running reaches the e1 node. This label features the <<>> operator that denotes an optional service call. Kmelia main vertical operators are: optional service call <<>> , optional behaviour insertion <||>, mandatory service call [[]], mandatory behaviour insertion [||]. An extended LTS is one in which the states and transitions may be annotated with subservices.

These structuring mechanisms provide a means to reduce the LTS size, to share common services or subservices and to master the complexity of service specification. This hierarchical behaviour structuring is naturally reflected in the service interfaces: this permits a precise description of the use of a subservice in the con- text of the interaction with a service. Both hierarchies must be consistent. Going one step further, they must be consistent with the link hierarchy of the component assemblies. This point will be one aspect of the compatibility property that will be discussed later in the paper.

The current version of the Kmelia language does not handle broadcast; this point and multi-way communications are subject to ongoing works. However we deal with the case where several services run simultaneously, as an interleaved behaviour plus synchronous communications on shared channels.

Dynamic Aspects Analysis within COSTO

In this section we focus on one dynamic property of components assemblies: checking that components interact well through their services.

We choose this property because it is complex and it illustrates the principle of connecting COSTO to others external powerful tools to run the effective verification of the property.

Analysis of Component Dynamic Aspects

The starting point is an assembly of components.

The interaction between the linked services implies a concurrent evolution of the services; this evolution is considered as a dynamic aspect of the component analysis.

Behavioural compatibility is about the correct interaction between two or more components which are combined via some of their services.

The behavioural compatibility analysis is performed by considering the correct interaction between the eLTS of the involved services.

It is a topic which is studied with several approaches [START_REF] Yellin | Protocol Specifications and Component Adaptors[END_REF][START_REF] De Alfaro | Interface Automata[END_REF][START_REF] Attie | Correctness of Model-based Component Composition without State Explosion[END_REF][START_REF] Bracciali | A formal approach to component adaptation[END_REF].

The main concern shared by these approaches is: checking that a given component interacts correctly with another one which may be provided by a third party developer.

In the Kmelia model, the interaction between components results in an interaction between linked services of the components. The interaction between components may involve not only two but many components.

But we consider only one caller service and one called service at the same time.

Therefore the component interacts correctly with its environment if its services are compatible with the other services with which they are linked.

The behavioural compatibility analysis is precisely formalised in [START_REF] Attiogbé | Checking Component Composability[END_REF]. We recall here the main idea.

A service is compatible with another if either their eLTSs evolve independently, in an interleaved way, or they perform complementary communication actions.

That is the basis of our compatibility analysis approach; we check that a given eLTS that models the behaviour of one service matches with a second eLTS that models the linked service behaviour.

A complete interaction between the services of several components results in a pairwise local analysis between the eLTS of a caller and that of the called service.

Two eLTS interact from their initial state until a terminal state according to a set of rules that we have defined.

The rules indicate the correct evolutions of the eLTS according to the current states of involved services and the labels of their transitions.

If the transitions are labelled with independent elementary actions, we have an interleaving of the independent actions of the transition systems.

If the transitions are labelled with communication labels involving the same channels, and the actions are complementary (an emission and a reception) then we have a synchronous communication involving the complementary actions.

If the labels are communication actions but not complementary, we get an incompatibility.

After a final state of a called service, the caller may continue with its independent transitions or with transitions that involve other (sub)services. After a final state of the caller the called service may continue only with elementary actions or with communication actions that do not need a complementary action from the terminated caller, otherwise we get an incompatibility. Practically, several points need to be considered to check the behavioural compatibility: various kinds of interactions, synchronous or asynchronous communications, atomic actions or composite ones.

Technically, checking the behavioural compatibility often relies on checking the behaviour of a (component based) system through the construction and the analysis of a global finite state automaton. However the state explosion limitation is a flaw of such an approach. We tackle this problem by considering local pairwise verification of behavioural compatibility: as a component provides several services in its interface, one has to select the service to be checked. Therefore only the links and sublinks of this service will be considered within a compatibility checking. Each service behaviour being encoded with an eLTS, we check only the eLTSs of the involved services. This local verification process may be iterated for each (linked) pair of services of the component assembly to perform a global checking.

Principle of Open Property Verification in COSTO

The effective verification of specification properties may require powerful systems such as model checkers or theorem provers. Implementing such tools requires much effort.

One major principle we adopted when building the COSTO toolbox is to open it to other languages, tools and environment in order to delegate various functionalities.

The application of this principle to the verification of dynamic properties currently leads to the LOTOS Analysis module and the MEC Analysis module (see Figure 1). The current section illustrates this principle. The analysis of properties which are specific to the Kmelia model are implemented as modules inside the COSTO toolbox; for example the composability of components is specific to Kmelia components, therefore composability checking is implemented as a specific COSTO tool. But the analysis of general properties or properties that can be translated into general ones is handled with available external tools. For example the behavioural compatibility of two eLTS is a general property that can be checked using existing tools such as MEC [START_REF] Arnold | Construction and Analysis of Transition Systems with MEC[END_REF] or LOTOS [START_REF] Garavel | An overview of cadp[END_REF].

For that purpose, connections with these tools are achieved. The part of the Kmelia specifications to be verified is translated into the input formalism of the targeted tool. The verification is then performed within the target environment. When possible, the feedback of such an external analysis is related to the Kmelia specification to help the specifier. We conducted various experiments with the reuse of existing tools. We used the MEC model checker [START_REF] Arnold | Construction and Analysis of Transition Systems with MEC[END_REF] to deal with behavioural part of Kmelia services. Using MEC we can focus specifically on service behaviours during preliminary analysis (where data is ignored). Some feedback from this analysis can help to correct the submitted specification. As far as two linked services (a caller and a callee) are concerned, we translate the LTS of each service into MEC automata, then the MEC synchronous product of both automata is built and then we search for deadlock freeness. The absence of deadlock implies the compatibility of the services. This experimentation with MEC has been reported in [START_REF] André | Vérification d'assemblage de composants logiciels Expérimentations avec MEC[END_REF]. We have also used the LOTOS/CADP toolbox [START_REF] Fernandez | CADP: A Protocol Validation and Verification Toolbox[END_REF][START_REF] Garavel | An overview of cadp[END_REF] as an external tool to conduct experiments on Kmelia specifications. We detail the connection between COSTO and CADP in the following section.

An External Module to Verify Service Interactions

In this section we explain how the CADP toolbox is connected to COSTO and how behavioural analysis is performed. Considering services to be checked for behavioural compatibility, the components that embody these services are first parsed by the Kmelia parser which generates their internal representation; the services involved in the analysis are extracted from the internal representation; then the extracted services are translated as LOTOS processes. To deal with behavioural compatibility we use the LOTOS selective parallel operator |[...]| to compose the generated LOTOS processes. This selective parallel composition operator is used because its semantics corresponds to our behavioural compatibility between services (see section 4.1); that is a synchronisation on specific selected actions and the interleaving of the other actions. The result of the translation and the composition of the processes are used as input of CADP tools.

LOTOS and CADP

LOTOS [START_REF] Lotos | A Formal Description Technique Based on The Temporal Ordering of Observational Behaviour[END_REF] is an ISO standard formal specification language. It is initially designed for the specification of network interconnection (OSI) but it is also suitable for concurrent and distributed systems. LOTOS extends the process algebra CCS and CSP and integrates algebraic abstract datatypes. A LOTOS specification is structured with process behaviours. It has the main behaviour description operators of the basic process algebra CCS and CSP. LOTOS uses the "!" and "?" operators of CSP which denote respectively emission and reception. The salient features of LOTOS are: the powerful multi-way synchronisation; the use of communication channels called gates; the synchronous interaction of processes; the use of algebraic data types to model data part of systems; the availability of a toolbox (CADP [START_REF] Fernandez | CADP: A Protocol Validation and Verification Toolbox[END_REF][START_REF] Garavel | An overview of cadp[END_REF]). CADP (Construction and Analysis of Distributed Processes) is the toolbox associ-ated to LOTOS; it enables one to apply its various model checking techniques on the described processes which are first compiled into labelled transition systems.

Translating the Kmelia Services into LOTOS Processes

Remind that the behaviour of each Kmelia service is modelled with an eLTS; the transitions of which are labelled with service calls, elementary actions, guarded actions and communication actions. Each state of the eLTS has an identifier. Some of the states are additionally labelled with a list of service names. We call an output transition of a given state a transition going from this state to another one. An input transition is a transition coming from any one state and entering another considered state.

The general principle of the translation (or encoding) is as follows. The input of the translation is the internal form of the transition system which describes a service. The internal form is the output of the Kmelia specification parser (CORE module). The input is translated into a LOTOS process.

We define a set of semantic encoding rules to support the translation of the component services into LOTOS. These semantic rules permit a systematic translation. Three kinds of encoding rules are defined: service interface translation, state translation rules (denoted by the LotosEncoding procedure) and transition label translation rules (denoted by the LotosEncodingL procedure). We do not give a full description of these rules (please see [START_REF] André | A Service-Based Component Model: Formalism, Analysis and Mechanization[END_REF]), but we give some illustrations of the approach used.

The translation of the data part of the Kmelia service results in LOTOS data types. To deal with communication, each service has a default channel with the same name as the service.

The translation of a transition system is achieved as follows. One main process is associated to the initial state of a transition system of a service and several related sub-processes are associated to the other states of the service. The processes have at least one parameter which is the default channel of the translated service; the abstract actions are collected as an alphabet that complements the process parameter.

A service without formal parameters (servName()) is called by sending its name on the default channel of the service; it is translated by: process servName[servName_chan, ...]: exit := servName_chan? varx: MsgTypeservName;[varx = servName];

A service with formal parameters is translated by a process which waits for the encoded service name and its parameters. Thus a service servName(p1: T1, p2: T2, ...) is translated by: process servName[servName_chan, ...]: exit := servName_chan? snx: MsgTypeservName; ? p1: MsgTypeservName; ?p2: msgTypeservName; [snx = servName] -> ...

From each state of the service there are one or several output transitions.

A state with several output transitions is translated by a non-deterministic choice between the translations of the output transitions; it results in a choice between as many process behaviour as possible in the LOTOS process. The translation into LOTOS of the transitions S0--act1-->fs1, S0--act2-->fs2 is the encoding of the S0 state: LotosEncoding(s0) = ( LotosEncodingL(act1); LotosEncoding(fs1) [] LotosEncodingL(act2); LotosEncoding(fs2) )

A state with more than one input transition is translated by a sub-process. Indeed, having more than one input transition means that the state can be reached from several transitions, therefore the sub-process is reused from different state translations.

A state annotated with a list of service names is translated by a non-deterministic choice between several sub-processes. Each sub-process corresponds to the interaction with one of the listed services. Consider the branching state S0 < <subserv1> >< <subserv2> >; if the service subserv1 is called, then the current service proceeds with the initial state in the subserv1. The encoding into LOTOS of S0 is as follows: LotosEncoding(initial_State(subserv2)) ) Endproc

The translation of labels is as follows. An elementary action is translated with an abstract action that will be an element of the process alphabet. As far as the guarded actions are concerned, first the guard is abstracted as an atomic element and then the guarded action gives a sequence of actions. Activations of service are treated as communication primitives. Communication actions are translated with LOTOS communication operators ! and ?.

According to the previous statements, we have formalised a specific semantic encoding (namely LotosEncoding) of the service specifications. Briefly, the encoding into LOTOS of service specifications is inductively performed by considering: service interface without formal parameters; service interface with formal parameters; service states (initial, final, intermediary and annotated) and service transitions.

For the translation of the data part of Kmelia services into LOTOS, we use enumerated types or bytes as data abstractions; the data values are then restricted in order to limit the state explosion problem. For each service, we define a specific LOTOS data type which has a constructor named with respect to the service; this permits the call of the service by sending its name on the convenient channel.

Besides, all the messages which are sent to the default channel associated to a service are used as constructors of the data type associated to this service. The expressions used within actions are translated as abstract actions of the alphabet of the LOTOS process.

After the translation process, we get full LOTOS processes which are used to check behavioural compatibility; they can also be analysed using various CADP verification modules.

Experimentation Results

The formal analysis using CADP starts after the generation of the LOTOS processes from the parsed Kmelia specifications of the involved components that embody the services.

To check the behavioural compatibility of a pair of services, the LOTOS processes resulting from their translation are composed with the |[alph]| operator to form a specific interacting system; alph is the action alphabet used for the synchronisation of the processes. The system obtained by composing the service processes is compiled with the CADP compiler caesar which also checks for the consistent use of the parallel composition operator. If the compilation is successful then the composition is correct hence the behavioural compatibility. If we have a deadlock from the compilation process due to communication actions mismatch then the processes are not compatible. This result is provided as feedback to the Kmelia specifier.

When there is no communication mismatch, caesar generates an internal graph (corresponding to the LTS) from which various analysis are available. For example the EVALUATOR module of CADP is used to model-check temporal properties (written in µ-calculus) that express safety or liveness properties on the service descriptions. More generally, all the analysis modules provided by the CADP tools are now made available due to the connection we have made through the translation into LOTOS. But in this case the specifier should move to the CADP environment.

Conclusion and Perspectives

We have presented an overview of the COSTO toolbox which supports the Kmelia abstract component model. The input of COSTO is Kmelia specifications.

Several modules are available within COSTO for parsing, behaviour visualisation, service or component interactions analysis.

The result of the Kmelia specification parsing is either used with the specific tools of COSTO or translated into the input formalisms of external tools.

We have emphasised the connection between COSTO and CADP by illustrating with the analysis of the behavioural compatibility analysis with the caesar compiler of the CADP toolbox after a translation of Kmelia service specifications into LOTOS processes. The COSTO toolbox is then connected to the CADP analysis framework after the generation of LOTOS processes. At the current stage of the COSTO development we focus on the use of model checking tools with respect to the behaviours of Kmelia services. Connections are made with the MEC tool and the CADP toolbox.

However, Kmelia component and service specifications are equipped with properties that appear as logical assertions. Therefore we begin a bridging with theorem proving tools such as that of the B Method.

For example, we have introduced protocols as user guides in the Kmelia model [START_REF] André | Defining Component Protocols with Service Composition: Illustration withe Kmelia Model[END_REF]; they are treated as specific services but their consistency is being studied using the assertions of the services which are to be translated in first order logic and proved correct with theorem proving. Most of the tools related to components and verification deal with dynamic checking techniques and use very abstract labelled transition systems or automata. Compared to Kmelia services, their descriptions are less expressive, this facilitates the related compatibility analysis; however they cover some aspects not yet covered by our framework. The VeSTA tool [START_REF] Bellegarde | The tool VeSTA: Verification of Simulations for Timed Automata[END_REF] checks the correct integration of a component (LTS) into a composite timed system. The SynCo tool [START_REF] Kouchnarenko | SynCo: a refinement analysis tool for synchronized component-based systems[END_REF] (Synchronized Component-based System Checker) implements a compositional analysis of the refinement of synchronized component-based systems (Automata). Weak and strict refinement relations are defined on components to allow proved transformations to code. The CHIC tool3 checks component interface compatibility in the sense of [START_REF] De Alfaro | Interface Automata[END_REF]. A refinement relation is defined in their approach but the tool is limited to behavioural compatibility checking with pushdown systems.The SOFA 2 4 component system provides an ADL-based design and a complete framework supporting all the stages of distributed applications lifecycle from development to execution. But the SOFA tools are specific to the SOFA component model [START_REF] Plasil | Behavior protocols for software components[END_REF] even if an integration to Fractal [START_REF] Bruneton | The Fractal Component Model[END_REF] has been studied. The Vercors platfom [START_REF] Barros | Model-checking distributed components: The vercors platform[END_REF] has a similar approach to ours; its is yet more mature than the COSTO toolbox. However the input component models of COSTO and Vercors are quite different and they need specific processing; for example, LOTOS specifications are directly used as component behaviour in Vercors whereas LOTOS specifications are generated for the services described with the Kmelia model. Moreover the Kmelia model and the related tools consider a correct development of components from their abstract specifications.

The perspectives of this work are: the bridging with the SOFA approach in order to share modules through our toolbox; the bridging with theorem proving tools to complement the property verification aspect for data-intensive systems and the enhancement of the data and assertion language of the Kmelia model for scalability. A methodological analysis process is needed to integrate the various verification modules; for example the combination of a mismatch detection with a module to guide the correction is viewed as the integration of a compatibility analysis tool with an adaptation tool. Furthermore we are working on a translation of a subset of Kmelia into the Fractal component model which has a Java execution environment but

Fig. 1 .

 1 Fig. 1. An overview of the COSTO Toolbox

Fig. 3 .

 3 Fig. 3. Overview of the ATM CORE component specification

Fig. 4 .Fig. 5 .

 45 Fig. 4. Overview of the Kmelia service syntax

Fig. 6 .

 6 Fig. 6. The withdrawal service eLTS (COSTO export)

  LotosEncoding(S0) = Process SP_Process_S0[...]: exit := ( chan_subserv1?fprm: MsgTypesubserv1 [fprm = subserv1]; LotosEncoding(initial_State(subserv1)) [] chan_subserv2?fprm: MsgTypesubserv2 [fprm = subserv2];

  COMPONENT ATM_CORE /* The ATM_CORE component is the central component for a bank cashier station.The main services of such a system are cash withdrawal, account query, deposit money and transfer bank query.

	The current specification focuses only on cash withdrawal. */
	INTERFACE
	provides : {withdrawal, account_query, deposit, transfer}
	requires : {ask_authorization, ask_account_balance}
	TYPES
	CashCard : struct {code:Integer, id:Integer, limit:Integer} // record type
	CONSTANTS
	// constants definitions
	available_cash : Integer := 100,
	swallowed_size : Integer := 100
	VARIABLES
	// variables definitions
	name : String,
	swallowed_cards : Set,
	available_notes : Integer
	PROPERTIES
	// predicates
	cash_disp: available_notes >= 0,
	card_capacity: size(swallowed_cards) <= swallowed_size
	INITIALIZATION
	// variables assignments
	name := "ATM203";
	swallowed_cards := emptySet;
	available_notes := 10000;
	SERVICES
	// services from external files (currently only in the same directory) can be included
	provided external account_query
	provided external deposit
	provided external transfer
	provided withdrawal (card : CashCard)
	// see the service withdrawal in Figure 4
	...
	//required services
	required ask_authorization (id : Integer, code : Integer) : Boolean
	...
	//internal services
	provided debit (c : CashCard, m : Integer)
	...
	END_SERVICES
	// end of ATM_CORE specification

  Provided withdrawal (card : CashCard) /* The service withdrawal is available if there is enough money in the cash dispenser.This services requires a bank credit card, a code, an amount to withdraw. An authorization is required from the bank consortium. This service provides an identification subservice if needed.

	*/
	Interface
	subprovides : {ident}
	calrequires : {ask_code, ask_amount} //required from the caller
	extrequires : {ask_authorization}
	Pre
	//service available if there is enough money
	available_notes >= available_cash
	Variables
	nbt : Integer,	// nbt : number of authorized trials of code entering
	c : Integer,	// c : input code given by the user
	a : Integer,	// a : input amount given by the user
	rep : Boolean,	// rep : reply from the authorization request
	success : Boolean // success : result of the withdrawal request
	Behaviour
	init i	// i is the initial state
	final f	// i is a final state
	{
	... see the service behaviour in Figure 6
	}
	Post
	available_notes <= pre(available_notes)
	// (success && (available_notes = pre(available_notes) -a)) ||
	// ((not success) && available_notes = pre(available_notes))
	end

pascal.andre@univ-nantes.fr, gilles.ardourel@univ-nantes.fr,christian.attiogbe@univ-nantes.fr

Additionally to provided services, Kmelia enables one to specify component protocols as special services.

http://www.eecs.berkeley.edu/∼arindam/Chic/

http://sofa.objectweb.org/

lacks property verification means. We expect some simulation facilities that will be complementary with the formal analysis aspect provided by Kmelia.


Mohammed El
email: mohammed.sehaba@liris.cnrs.fr

Amine Sehaba

Carlos F Crispim-Junior
email: carlos.crispimjunior@liris.cnrs.fr

Laure Tougne Rodet

Embedded plant recognition: a benchmark for low footprint deep neural networks

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Our relationship with nature has profoundly changed in recent decades. While less than a third of the world's population lived in cities in 1950, this will be the case for more than two thirds of the population in 2050 [START_REF]World urbanization prospects[END_REF]. Human is therefore moving further and further away from nature.

Paradoxically, he has understood that he must protect his environment to survive. But we can only protect what we know well. In other words, environmental education is essential. It is therefore essential to learn to know the plants that surround us. This learning can be done through computer tools and especially smartphones that everyone now has in his pocket.

There exist many plant recognition applications freely available like Pl@ntNet Identify [8], Seek [START_REF] Seek | [END_REF], Pic-tureThis [START_REF]Picturethis[END_REF], LeafSnap [5], Google Lens [START_REF]Google lens[END_REF], etc. but all these applications require a working Internet connection since the classification task is processed on a remote server. But in the nature, in the forest, in the mountains, etc. we do not necessarily possess an Internet connection. This implies to have embedded recognition algorithms. In this context, trade-offs must be made between response accuracy, processing speed and memory footprint. The only plant recognition application currently available that works without an Internet connection is InterFolia [START_REF]Interfolia[END_REF].

The objective of this work is precisely to compare different possible network models for the embedded recognition of trees and shrubs on the same dataset which contains many species (up to 184 per organ) and for which it is possible to use different organs (leaf, bark, flower/fruit).

In the remainder of this paper, we will first briefly de- scribe the state of the art that on embedded plant recognition. We will then present the dataset that we have proposed to establish these performance comparisons. We will describe the architectures of the deep neural networks we have chosen to compare and justify this choice. The section 5 will present the different experiments conducted and the results obtained.

Related work

Automatic plant recognition is a very developed research topic since many years [START_REF] Rajeesh | Automatic plant recognition : A review[END_REF]. It is a difficult problem for multiple reasons: firstly, there are many plant species in nature, which results in many classes to discriminate. It is estimated that there are 400,000 species of plants in the world. Second, some species are not frequent and therefore we sometimes have very few examples per class. Third, some species have organs that may be visually quite different (Figures 1 and2). It conducts to a very important intra-class variability. In the same way, we can have organs of different species which are very similar to each other (Fig. 1, right image); which has for effect also a similarity inter-class sometimes very important. In addition to this, the images are taken in an uncontrolled environment, which can lead to artefacts of luminosity or cast shadows that can disturb recognition. Figure 3 shows the large variability of shape and color within flowers/fruits.

The methods developed in the literature were initially based on the segmentation of the object to be recognized, extraction of handcrafted features and classification of the resulting feature vectors [16,18,[START_REF] Le | Complex background leaf-based plant identification me-thod based on interactive segmentation and kernel descriptor. 2nd International Workshop on EMR[END_REF][START_REF] Nguyen | A combination of deep learning and hand-designed feature for plant identification based on leaf and flower images[END_REF]. The main problem with this type of methods was its sensitivity to segmentation quality. Indeed, poor segmentation implied features that did not really correspond to the object, and consequently lead to potential misclassification. Then, deep learning based methods took over, as in other application fields, and are now the only ones used [START_REF] Giguere | Tree species identification from bark images using convolutional neural networks[END_REF][START_REF] Misra | Patch-based CNN evaluation for bark classification[END_REF]12,[START_REF] Saadeh | Flower classification using deep convolutional neural network[END_REF]. However, as deep learning methods are often computationally and memory-intensive, they are still very often deployed in remote servers.

The development of smartphone applications has given rise to numerous applications that are either dedicated to plants (e.g. PlantNet identify), or that allow to recognize anything and in particular plants (e.g. Google Lens application). Initially based on the extraction of handcrafted characteristics, most of these applications are now based on deep learning methods. The principle is the same for all of them: the user classification request is sent to a remote server which processes the image and sends the answer back to the smartphone. This framework allows to use "large" deep neural networks and powerful computing servers to run the classification task. However, as in nature we often have either very little Internet connection or no connection at all; these applications are incompatible with this context of use. The only existing application that does not require an Internet connection is InterFolia [START_REF]Interfolia[END_REF] which embeds SqueezeNet networks because of their small size and fast response time [START_REF] Langlade | InterFolia: an embedded, educational application to identify plant species in the wild[END_REF]. More specifically, three models are on board: one for recognizing leaves, one for barks and one for flowers and fruits. The user can take several photos of the different organs of the same plant and ask the application to combine the results.

But is this network architecture still the most suitable to address the problem? Can more recent network architectures be embedded in the current smartphones? For instance, there are many "small" networks architecture that are good candidates for the task, such as MobileNet family (V2, V3) [START_REF] Zhu | Mobilenetv2: Inverted residuals and linear bottlenecks[END_REF]14], EfficientNet [32], SqueezeNet [21] or MobileViT [START_REF] Sachin | Mobilevit: light-weight, general-purpose, and mobile-friendly vision transformer[END_REF]. However, given the difficulty of the plant recognition problem, it is difficult to predict which network would be the most suitable. Comparisons made in other contexts, such as, manufactured objects, do not correspond to the conditions we experience in the context of plant recognition in natural environments. For these reasons, we propose InterFolia 2.0, a novel performance benchmark for plant recognition task.

Datasets

There are many datasets in the literature concerning plant species (Table 1). Several datasets contain a single organ. For instance, leaves [START_REF] Gang | A leaf recognition algorithm for plant classification using probabilistic neural network[END_REF], barks [START_REF] Porebski | A new benchmark image test suite for evaluating color texture classification schemes[END_REF][1]), or flowers and fruits ( [START_REF] Oxfordflower | [END_REF][2] [START_REF]Fids30[END_REF]). However, in [START_REF] Gang | A leaf recognition algorithm for plant classification using probabilistic neural network[END_REF], for example, the leaves are shot flat against a white background, which is not representative of real-life conditions. In [START_REF] Oxfordflower | [END_REF], these are ornamental flowers that are photographed, not tree or shrub flowers. There exist also datasets mixing organs such as [19]. However, most of these datasets do not contain many classes and therefore do not cover all the trees and shrubs that can be found on a territory like France for example.

The datasets used in the ImageClef challenges2 are rather complete but do not differentiate the plant organs. Even if a user may not be able to tell the difference between a flower and a fruit from trees and shrubs due to its similarity for non-experts, it is easy to tell the difference between a leaf and a bark, a leaf and a fruit, or a leaf and a flower. Thus, aiming at a smartphone use, we can consider recognizing specifically these types of organs. Indeed, we can easily ask the user to specify if the picture taken is of a leaf, a bark or a flower/fruit. The idea is that by using a model per plant organ, one hopes to recognize plant species more easily. Prior work has shown that using several organs of the same plant to recognize the plant species improves the results [START_REF] Langlade | InterFolia: an embedded, educational application to identify plant species in the wild[END_REF].

For this, we require a dataset that organizes the images of each plant species per organ. However, the only dataset

Dataset # of images # of classes Barks Leaves Flowers/Fruits

Bark-101 [1] 2.5k 101 X - - BarkNet [15] 23k 23 X - - BarkID [31] 18k 10 X - - Flavia [28] 1.9k 32 - X - Leafsnap [5] 28k 184 - X - Oxford-102 [6] 8k 102 - - X InterFolia [33] 9k 477 X X X
Table 1. Existing plant datasets. The letter "X" denotes available information.

known to us with plant photos classified by species and organs is the dataset used by the InterFolia application, that is currently a private dataset. have been classified by organ, in addition to species. Table 2 presents the distribution of the dataset for the different organs, as well as the number of species. We observe that there are fewer bark classes than leaf or flower/fruit because bark has no meaning for shrubs. We may also notice that InterFolia dataset is very unbalanced. For some classes, we have only 2 examples which is clearly insufficient to learn the variability of the organs. The left image of Figure 1 shows pictures of barks of the same species. We understand that with 2-3 photos per class (an organ of a species), a datadriven method, such as a deep neural network, is likely to face difficulty to learn a species model for accurate recog-nition.

InterFolia dataset

InterFolia dataset 2.0

This section describes how we extended InterFolia dataset to obtain a richer version, for bark class recognition. The resulting dataset called InterFolia dataset 2.0 is available to the community on Kaggle. Firstly, we removed from the dataset the classes that contained less than 3 examples. This is done to be sure to have at least one image is available for the training, validation, and test sets.

Bark-101 dataset [START_REF] Ratajczak | Efficient Bark Recognition in the Wild[END_REF] is also based on PlantCLEF dataset and it contains 101 tree bark classes on which the authors compared different recognition methods.

We merged both datasets to create InterFolia 2.0. This allowed us to get more classes and examples for barks. We have removed any duplicates that we found. Additionally, we have removed all shrub images in the Bark 101 dataset, to focus only on bark images of older trees. Table 3 We can see that we have a dataset with 477 classes (167 leaves, 181 flowers/fruits, 129 barks) and 10058 examples. This is already an interesting challenge in terms of classification when we know the nature of the objects to recognize, and the material constraints imposed by the smartphone. Figure 4 shows the class distribution for each organ type. We can see that the classes are also imbalanced, and that this remains a major challenge to overcome to achieve good recognition rates.

Finally, all the three new datasets were divided into train, validation, and test sets. At first, we split the dataset into 70% of images for training and 30% for testing. Then, the train set is divided again into 70% for training and 30% for validation. In the following, we focus on the architectures we compared and their training conditions.

Architectures and pretrained models

Using embedded networks necessarily involves tradeoffs between performance, network size and inference time.

We first chose networks that are "light" in terms of memory impact but efficient. We also considered that it was important to compare them with "trendy" networks, like visual Transformers. Finally, we also added in our comparison the SqueezeNet network which is the network architecture currently used in the InterFolia application.

Table 4 compares the selected networks in terms of number of parameters, model size and efficiency on the Ima-geNet dataset 3 . Notice that the 'TOP-5' error rate is the fraction of test images for which the correct label is amongst this top 5, and the 'TOP-1' error rate is the fraction of test images for which the correct label is the one judged most likely by the model.

Inference time of the four selected pre-trained models is counted in milliseconds [START_REF] Zhu | An improved one millisecond mobile backbone[END_REF]. MobileNet V2 [START_REF] Zhu | Mobilenetv2: Inverted residuals and linear bottlenecks[END_REF] This model achieves a better accuracy on ImageNet than MobileNet V2. We therefore propose to compare the two architectures on our problem. In [32], T. Mingxing and Q. Le introduced a new family of neural networks called Effi-cientNet. EfficientNet architectures are very efficient computationally and achieves state-of-the-art results on the Ima-geNet dataset. Thus, we propose to compare the results obtained with the EfficientNet-B0 architecture. Finally, we include in this study a very small network (SqueezeNet [21]) which does not give very good results on ImageNet but which has the merit of not taking too much memory space. It is the architecture the authors of InterFolia have adopted. At the opposite end of the spectrum, we include a large, trendy network, MobileViT [START_REF] Sachin | Mobilevit: light-weight, general-purpose, and mobile-friendly vision transformer[END_REF].

Experiments and results

Note that all models are based on PyTorch framework, and they were pre-trained on ImageNet. For the evaluation of models on the smartphone, we converted all models using CoreML framework [START_REF]Coremltools[END_REF].

Training details and evaluation criteria

For the three sub-datasets, we use the software library Albumentations4 for data augmentation. For both leaf and bark datasets, we train our models for 50 epochs, with a batch size of 32, and a learning rate of 1e-4 that decreases by 0.1 every 7 epochs. We apply categorical cross-entropy loss function and Adam optimizer. For the Flowers/Fruits dataset, we use the same training hyperparameters of other organ models, except that we train models for 10 epochs, with a batch size of 128.

We evaluate our models on several criteria. First evaluation criterion is the efficiency of the network, for that, we calculate the TOP-1 and TOP-5 accuracy. Secondly, since the target phones are limited in hardware resources, we take into consideration the memory size of the model, to ensure that the 3 networks (one per organ) can be embedded in addition to the elements necessary for the proper functioning of the application (example of images to be shown to the user for instance). The third criterion is the inference time of the network to ensure that the user will not have to wait too long for the result of his request.

Results and discussion

First, we present the results obtained using PyTorch models on a MacBook computer. The MacBook configuration is not relevant because our goal here is to establish a baseline in terms of memory size and accuracy, that will be later compared with the embedded version of the models running on the device. Then, we convert those models to be compatible with an iPhone 12 Pro. This smartphone model has an Apple A14 Bionic processor equipped with 6 GB of RAM. The Apple A14 Bionic has a six-core 64-bit processor implementing ARMv8 ISA and incorporates a four-core @1000 MHz graphics processor designed by Apple. We convert all trained models to "neuralnetwork" type using CoreML-Tools, and allow it to use all compute units available on the target device.

The aim here is to compare the converted models in terms of memory size, accuracy, and inference time.

Results on the computer

Tables 5, 6 and 7 present the models' results, respectively, on Leaves, Flowers/Fruits and Barks datasets. We compare models of the following architectures: MobileNet versions 2 (MV2) and 3 (MV3), EfficientNet version B0 (EB0), Mobile ViT (MViT) and SqueezeNet (SQ). First, bark recognition is much more difficult than leaf or flower/fruit recognition. This is mainly because the shape of leaves is very characteristic. For flower/fruit, color is an important piece of information in addition to shape. bark, color is not very discriminating, and only texture is. Moreover, texture varies over time with the age of the plant. On Leaves dataset, the three networks MobileNet V3, EfficientNet-B0 and MobileViT-S are equally effective, but MVIT is slightly larger. MobileNet V2 has a lower efficiency than the other 3 architecture but it is almost half their size. SqueezeNet achieves very low performance.

Model Memory size

On Flowers/Fruits dataset, EfficientNet-B0 is the best while MobileNet V3 and MobileViT-S are equivalent. SqueezeNet's performance is still well below other networks.

Finally, on Barks dataset, MobileNet V3 is the best networks with MobileViT-S not far away but still with a larger size. EfficientNet-B0 has a little low performance on barks. SqueezeNet is still well below in terms of performance.

To conclude on these first tests, EfficientNet-B0, Mo-bileNet V3 and MobileViT-S are the best performing methods; MobileViT-S remains the largest with the most parameters.

Results on the smartphone

Tables 8, 9 and 10 show the obtained results using the models converted to CoreML and running on a smartphone. We did not provide results for MobileViT model here because the other architectures we tested presented a higher performance with a smaller number of parameters.

First, we note a small overall loss of performance for all models on the flowers/fruits and barks datasets. On the leaves dataset, performance is slightly better on the smartphone, but we did not run the experiment many times. We therefore conclude that the results are broadly equivalent to those obtained on the computer.

Concerning the Leaves dataset, the best network is clearly EfficientNet-B0 both in terms of performance and inference time. MobileNet V3 has a much higher inference time. MobileNet V2 has an interesting inference time, and a lower memory impact but it achieves a lower performance. On flowers/fruits dataset, EfficientNet-B0 remains the best compromise, as we observed during the experiment on the computer. Finally, it should be noted that MobileNet V2 has a very good behavior on the barks dataset which is a difficult dataset.

To conclude from these tests, the first element that comes out is that the bark dataset is very challenging. MobileNet V2 is recommended in this context for its performance, its inference time, and its memory impact.

For the other two sets (flowers/fruits and leaves), EfficientNet-B0 is the best compromise. SqueezeNet really does not seem to be the better solution for this problem, since its performances are very low.

Conclusion and future Work

In this paper, we presented a benchmark of model comparisons for embedded plant recognition.

We first proposed a dataset organized by species and organs that will be made available to the scientific community. This dataset is very challenging as recognizing plants in natural environment is. It also contains lots of classes for each organ and imbalanced classes. Efficiently combining the results from 2 or 3 organs of the same plant remains a challenge too in this context. The effectiveness of new methods can therefore be tested on this difficult dataset.

Secondly, we compared most interesting models of the literature to solve the problem of embedded plant recognition. The results show that depending on the type of organ to recognize, the same network is not always recommended.

For organs that can be discriminated by their shape and color like leaves or flowers/fruits, EfficientNet-B0 is a good solution. For barks, which are more difficult to discriminate and based on texture, MobileNet V2 is interesting.

In any case, the SqueezeNet network currently used in the InterFolia application is not the one that achieves the best results. It might be worthwhile to change the networks embedded in InterFolia and study the benefit in terms of recognition.

It should be noted that these results obtained on tree and shrub organs found in metropolitan France are exportable to organs of other plant types. They could thus serve as a basis for embedded phenotyping research in other contexts.

In future work, research can be undertaken on the most efficient use of the results of the different classifiers. It will also be necessary to work on methods to overcome the lack of data on certain classes to improve the results.

Figure 1 .

 1 Figure 1. Examples of bark images from (left) the same species, (right) two different species.

Figure 2 .

 2 Figure 2. Examples of leaf images from InterFolia dataset: the 4 images are from the same species.

Figure 3 .

 3 Figure 3. Examples of flower/fruit images from InterFolia dataset to show variability.

Figure 4 .

 4 Figure 4. Distribution of classes in InterFolia dataset 2.0.

  was introduced by M Sandler et al. in 2018. This architecture is suitable for Mobile devices, or any devices with low computational power. In [14], A. Howard et al. have introduced a new version of MobileNet, that they called MobileNet V3.

  This ICCV workshop paper is the Open Access version, provided by the Computer Vision Foundation. Except for this watermark, it is identical to the accepted version; the final published version of the proceedings is available on IEEE Xplore.

Table 2 .

 2 The Interfolia dataset has been used to train the deep neural network models used by the InterFolia application. It is based on the ImageCLEF dataset in which the examples Composition of the InterFolia dataset

	Organs	Barks Leaves Flowers/Fruits
	# Images	1,236	2,536	5,245
	# Species (classes)	148	178	184
	# classes with 2-10 samples	118	107	51
	# classes with 11-50 samples	25	66	107
	# classes with 51-311 samples	5	5	26

  presents the number of classes and samples per organ of the created dataset.

	Dataset	# classes # samples
	Leaves	167	2,514
	Flowers/Fruits 181	5,239
	Barks	129	2,305

Table 3 .

 3 Number of images for each organ.

Table 5 .

 5 Leaves -Results using models on MacBook.

	Model Memory size TOP-1	TOP-5
	MV2	10.1 MB	45.10% 70.10%
	MV3	17.9 MB	48.28% 71.18%
	EB0	17.2 MB	53.31% 75.45%
	MViT 20.6 MB	48.21% 71.82%
	SQ	3.3 MB	13.36 % 27.54%

Table 6 .

 6 Flowers/Fruits -Results using models on MacBook.

Table 7 .

 7 Bark -Results using models on MacBook.

Table 8 .

 8 Leaves -Results using models on iPhone 12 Pro.

	Model Mem size Inference time TOP-1	TOP-5
	MV2	9.7MB	2.04ms	46.88% 66.22%
	MV3	17.6MB	21.42ms	50.99% 69.66%
	EB0	16.8MB	2.62ms	50.59% 67.68%
	SQ	3.3MB	1.24ms	12.31% 23.97%
	Model Mem size Inference time TOP-1	TOP-5
	MV2	9.8MB	2.03ms	42.74% 68.23%
	MV3	17.7MB	21.65ms	46.47% 70.26%
	EB0	16.9MB	2.67ms	51.50% 75.49%
	SQ	3.3MB	1.23ms	12.81% 27.97%

Table 9 .

 9 Flowers/Fruits -Results using models on iPhone 12 Pro.

	Model Mem size Inference time TOP-1	TOP-5
	MV2	9.5MB	1.86ms	29.57% 48.02%
	MV3	17.4MB	21.56ms	30.16% 48.16%
	EB0	16.6MB	2.66ms	26.20% 45.53%
	SQ	3.2MB	1.23ms	16.25% 29.06%

Table 10 .

 10 Bark -Results using models on iPhone 12 Pro.

https://www.imageclef.org/

https://pytorch.org/vision/stable/models.html

https://albumentations.ai/docs/

://kaggle.com/datasets/lauretougne/interfolia


Maroua Lejmi

Damien Geslin

Ilef Bertrand Cuissart

Ben Slima

Nida Meddouri

Ronan Bureau

Alban Lepailleur

Amel Borgi

Jean-Luc Lamotte

Refinement of a ligand activity and representation of topological pharmacophores in a colored network

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Pharmacophore evaluation: "Adapted Growth-Rate" SAR : better understanding of association between pharmacophores and ligand affinity.

Refinement of a ligand activity and representation of topological pharmacophores in a colored network

Maroua Lejmi 1,4 , Damien Geslin 2 , Bertrand Cuissart 1 , Ilef Ben Slima 3 , Nida Meddouri 6 , Ronan Bureau 2 , Alban Lepailleur 2 , Amel Borgi 5 , Jean-Luc Lamotte 1 1 Equipe CODAG -Laboratoire GREYC -UMR6072 -Groupe de Recherche en Informatique, Image et Instrumentation de Caen -France 2 Centre d'Etudes et de Recherche sur le Médicament de Normandie -Université de Caen Normandie : UR4258, Université de Caen Normandie -France 3 3 ISMAIK, University of Kairouan, Digital Research Center of Sfax (CRNS), SM@RTS, Sfax, Tunisia 4 FST-LIPAH / Université de Tunis El Manar, Tunis, Tunisie 5 ISI-LIPAH / Université de Tunis El Manar, Tunis, Tunisie 6 Laboratoire de Recherche de l'EPITA (LRE), Le Kremlin-Bicêtre, France.

Context and Goal

The Pharmacophore Network [2]: a graph of pharmacophores whose nodes represent the pharmacophores and edges represent the distance of similarity between them determined through similarities between the supporting molecules.