Pascal André

Gilles Ardourel

Christian Attiogbé

Arnaud Lanoix

Using Assertions to Enhance the Correctness of Kmelia Components and their Assemblies

Keywords: Component, Assembly, Datatype, Assertions, Property Verication

The Kmelia component model is an abstract formal component model based on services. It is dedicated to the specication and development of correct components. This work enriches the Kmelia language to allow the description of data, expressions and assertions when specifying components and services. The objective is to enable the use of assertions in Kmelia in order to support expressive service descriptions, to support client/supplier contracts with pre/post-conditions, and to enhance formal analysis of component-based system. Assertions are used to perfom analysis of services, component assemblies and service compositions. We illustrate the work with the verication of consistency properties involving data at component and assembly levels.

Introduction

The Kmelia component model [?] is an abstract formal component model dedicated to the specication and development of correct components. A formal component model is mandatory to check various kind of properties for component-based software systems: correctness, liveness, safety; to nd components and services in libraries according to their formal requirements; to rene models or to generate codes.

The key concepts of the Kmelia model are services, component, component assembly and component composition. One important feature of the Kmelia model is the use of services as rst class entities. A service has a state, a dynamic behaviour which may include communication actions, an interface made of required, provided and subservices. Component composition is based on the interaction between linked services which form a component assembly. This use of services constitutes a bridge to service oriented abstract models.

In [?] we introduced the syntax and semantics for the core model and language.

It has been incrementally enriched later. We mainly focused on the dynamic aspects of composition: interaction compatibility in [?], component protocols with service c 2009 Published by Elsevier Science B. V.

composition in [?] and multipart interaction with synchronous communication and shared services in [?]. Following this incremental approach, we consider in this article an enrichment of the data and expressions in the kmelia model and its impact on the language syntax, its semantics and the verication of properties. Our guiding objective is twofold: 1) enable the denition of assertions (with invariant, pre/post conditions, and properties of services, components, and compositions), 2) to increase the expressiveness of the action statements so as to deal with real size case studies.

Assertions are useful (i) to dene contracts on services; contracts increase the condence in assembly correctness and they are a pertinent information when looking for candidates for a required service, (ii) to ensure the consistency of components respecting the invariant. The actions implement a functional part of the services which should then be proved to be consistent with the contracts. Therefore the correctness verication aspects of the Kmelia model is enhanced.

Motivations. Modelling real life systems requires the use of data types to handle states, actions and property descriptions. The state of the art shows that most of the abstract components models [?,?,?,?,?] focus mainly on the dynamic features.

They enable various verications of the interaction correctness but they lack expressiveness on the data types and do not provide assertions mechanisms and the related verication rules. As an example, in Wright the dynamic part based on CSP is largely detailed (specication and verication) while the data part is minor [?].

In [?] the data types are dened using algebraic specications, which are convenient to marry with the symbolic model checking of state transition systems. But this model does not support contracts and assertions.

Contribution. In this work, we enrich the model with data and assertions at service and composition levels in order to deal with safe services, component consistency and assembly contracts. First, the Kmelia language is enriched with data and assertions so as to cover in an homogeneous way structural, dynamic and functional correctness with respect to assertions. Second, we deal with state space visibility and access through dierent levels of nested components; in addition to service promotion we dene variable promotions and the related access rules from component state in component compositions. Last, feasibility of proving component correctness using the assertions is presented. We show how structural correctness is veried and how the associated properties are expressed with the new data language.

The article is structured as follows. Section ?? gives an overview of the Kmelia abstract model and introduces its new features. In Section ?? a working example is introduced to illustrate the use of data and assertions. The formal analysis issue is treated in Section ??; we present various analysis to be performed and we focus on component consistency and on checking assembly links. Section ?? concludes the article and draws some discussions and perspectives.

The Kmelia Model and its new Features

This section recalls the main features of Kmelia. The core concepts are component, services, component assembly and composition [?]. Now, the Kmelia language allows the description of datatypes, expressions and rst order logic predicates. We describe the Kmelia model, focusing on its new features.

Data types and expressions

To design the Kmelia data language, we have established a trade o between the desired expressiveness of our language and the verication concerns. We tried to encapsulate statements from other formal data languages such as Z, B, OCL or CASL, with the idea to reuse existing tool supports for checking syntax and properties, but this approach was not convincing due to expressiveness, syntax and semantics conicts between the used languages. To avoid the separation of analysis tools and to work on the same abstract model, we advocate for an approach where both data and dynamic part are integrated in a unique Kmelia language. We enrich the Kmelia language by designing a small but expressive data language. This enables us to deal homogeneously with the expression of the properties related to the component level and to the composition level.

Basic types such as Integer , Boolean, Char, String with their usual operators and standard semantics are permitted. Abstract data types like record, enumeration, range and collection (arrays, sets) are allowed in Kmelia. User-dened record types are built over the above basic types. Specic types and functions may be dened and imported from libraries. A Kmelia expression is built with constants, variables and elementary expressions built with standard arithmetic and logical operators.

An assignment is made of a variable at the left hand side and an expression at the right hand side.

Assertions (pre-/post-conditions and invariants) are rst order logic predicates.

In a post-condition of a service, the keyword old is used to distinguish the before and after variable states. This is close to OCL's pre or Eiel's old keywords. Guards in the service behaviour (eLTS) are also predicates. All the assertions are governed by an observability policy described in Section ??.

Components

A component is one element of a component type. A component is referenced with a variable typed using the component type; for example c :C where c is a variable and C a component type. The access to a state variable v of c is denoted c .v.

A component type C is a 9-tuple W, Init, A, N , M, I, D, ν, CS with:

• W = T, V, type, Inv the state space where T is a set of types, V a set of variables, type : V → T the function that map variables to types and Inv an invariant dened on V . • Init the initialisation of the variables of V .

• A a nite set of elementary actions.

• N a nite set of service names. Let N P (provided services) and N R (required services) be two disjoint nite sets of names 1 : N = N P N R . • M a nite set of message names.

• I = I P I R the component interface which is the union of two disjoint nite sets of names I P and I R such that I P ⊆ N P ∧ I R ⊆ N R .

denotes the disjoint union of sets

• D is the set of service descriptions; it includes the provided services (D P ) and the required services (D R ).

• ν : N → D is the function mapping service names to service descriptions. Moreover there is a projection of the N partition on its image by ν:

s ∈ N P ⇒ ν(s) ∈ D P ∧ s ∈ N R ⇒ ν(s) ∈ D R
• CS is a set of constraints related to the services of the interface of C in order to control the usage of the services.

Observability of the component state. The subsets form a partition of V . Particularly, pre-/post-conditions and the state invariant Inv are composed of an observable (I nv O dened on V O ) and a non-observable part.

Services

The behaviour of a component relies on the behaviours of its services. A (sub-)service models a functionality activated by a call. A service may activate other services during its evolution. Due to dependencies between services and interaction between components, the actions of several activated services may interleave or synchronise.

Only one action of an activated service may be observed at time. Formally a service s of a component type C2 is dened by a 4-tuple IS, lW, lInit, B with:

• The service interface IS is dened by a 6-tuple σ, µ, vW, P re, P ost, DI where

• σ is the service signature name, param, ptype, res with name ∈ N , param a set of parameters, ptype : param → T the function mapping parameters to types and res ∈ T the service result type;

• vW = vT, vV, vtype, vInv is a virtual state space with vT a set of types, vV a set of variables, vtype : vV → vT the function mapping context variables to types and vInv an invariant dened on vV ; • µ is a set of message signatures mname, mparam, mptype where mname ∈ M, mparam and mptype are similar to those of the service signature; • P re is a pre-condition dened on the union (∪) of the variables in V, vV, and param: V ∪ vV ∪ param;

• P ost is a post-condition dened on V ∪ vV ∪ param ∪ { result };
• DI is the service dependency; it is composed by services on which the current service depends on. DI is a 4-tuple sub, cal, req, int of disjoint sets where sub ⊆ N P (resp. cal ⊆ N R , req ⊆ N R , int ⊆ N P ) contains the provided services names (resp. the ones required from the caller, the ones required from any component, the internal services) in the scope of s.

• lW = lT, lV, ltype, lInv is the local state space where lT is a set of types, lV a set of local variables, ltype : lV → lT the function mapping local variables to types and lInv a local state invariant dened on lV (mostly lInv = true).

• lInit the initialisation of the variables of lV .

• The behaviour B of a service s is an extended labelled transition system (eLTS), detailed in [?,?,?]. A transition label is a combination of actions; it can be guarded.

The actions are either elementary actions from A or communication actions (to call/to end a service, to send/to receive a message).

Virtual state spaces. As a required service is an abstraction of a service oered by another component, it is necessary to describe this imaginary component. We introduce the notion of a virtual state space vW in order to abstract a service from its denition context which is a component. For a provided service this virtual context is always empty.

V O V Inv O Inv Required s vV V vInv Inv
The pre-/post-conditions of s must respect the well-formedness rules related to the observable, non-observable and virtual contexts according to the following table :   Service pre-condition post-condition Assertions Observable Non-observable Observable Non-observable scope

P re O P re N O P ost O P ost N O Provided s V O ∪ param none V O ∪ param ∪ { result } V ∪ param ∪ { result } Required s vV ∪ param V ∪ param vV ∪ param ∪ { result } none
The other cases not detailed in the table are summarised in Figure ?? which describes: an abstract view of the variables of a component, their scopes and the assertion scopes; it also depicts how these contexts are used in assembly and composition.

Fig. 1. State variables scope and assertion scope

3 it is not a partition here because of the supplementary variables in param and result

The observable pre-/post-conditions will be used to check the assembly contracts and the promotion contracts. Non-observable pre-conditions (resp. post-conditions) are meaningless for a provided service (resp. required service) because they prevent safe assembly and promotion contracts. The non-observable pre-condition of a required service gives call conditions on the (caller) component state variables.

The non-observable post-condition of a provided service should establish the nonobservable part of the invariant.

The state space lW local to a service is used only in the service behaviour B but not used in the assertions.

Assembly and Composition

An assembly is a set of components that are linked (horizontal composition) through their services. An assembly is one element of an assembly type. An assembly link associates a required service to a provided one. Considering the rich interface of a Kmelia service (see ??), we need an explicit matching mechanism, to link properly the 6-tuples dening given services; therefore, additionally to signatures and dependency (via sublinks) mapping we now dene context and message mappings.

vV sr → exp(V O CP )
where exp(X) denotes an expression over the variables of X. Each message name of sr is mapped to a message name of sp by a mapping (total) function mmap : mname sr → mname sp .

A composition is the encapsulation of an assembly into a component (the composite) where some features (variables and services) of the nested components can be promoted to the composite level. Promotion links are used to promote provided or required services. The mappings and rules are similar to the ones of assembly, they are not detailed here. This guarantees the encapsulation principle. Now Kmelia services are equipped with expressive means (pre-/post-conditions, observability, virtual context) to describe contracts. Section ?? illustrates them on a working example. They are used to check services and assemblies correctness as described in Section ??.

State variables promotion. An observable variable vo

∈ V O C from a component

A Working Example

The example is a simplied Stock Management application including a vending process as a main service. This process manages product references ( catalog) and product storage (stock). Administrators have specic rights, they can add or remove references under some consistency business rules such as: a new reference must not be in the catalog or a removable reference must have an empty stock level. Vendor. The former one is the core business component to manage references and storage.

The latter one is the system interface which main service, the vending service, is promoted at the StockSystem level. In this paper we focus on the vending and newReference services, the other services will not be more detailed further. With respect to vending, a user may add a new item in the stock management system; a new reference, and a quantity is required for the added item. In the design system the Vendor component requires a service addItem which will get a new reference and perform the update of the system. This simple functionality may fail if there is no available new reference.

The required service addItem is fullled with the provided service newReference.

The links and sublinks are explicitly dened in the composition part of a composite component, as detailed in the listing ??.

The nested services represent the service dependency DI. For example, the required service addItem provides a special code subservice4 . Similarly the provided service newReference requires a ask_code service from its caller (see the calrequires declaration in the interface of newReference in the listing ??).

Inside the components, the dierent arrows represent various kind of calls: function call (with no side eects), service call (according to the service dependency).

The newReference service calls the primitive display function (declared in the predened Kmelia library), an internal service getNewReference // f i l l e d by a required s e r v i c e p l a b e l s:= a r r a y I n i t ( p l a b e l s , e m p t y S t r i n g ) ; // c o n s i s t e n t with . . p s t o c k := a r r a y I n i t ( p s t o c k , n o Q u a n t i t y ) ; // . . empty catalog A Kmelia service with its assertions. The listing ?? gives the specication of the provided service newReference. It provides a new reference if its running goes well. The pre-condition is that the catalog does not reach its maximal size. The post-condition is decomposed into several observable/non-observable named parts.

It states that we may have a result ranging in 1. .maxRef or no reference at all, in the latter case the catalog remains unchanged.

Andre et al.

Listing 2: Kmelia specication Provided Service with assertions provided n e w R e f e r e n c e ( ) : I n t e g e r // Result = ProductId or noReference I n t e r f a c e c a l r e q u i r e s : { ask_code } #required from the c a l l e r i n t r e q u i r e s : { g e t N e w R e f e r e n c e } Pre obs s i z e ( c a t a l o g ) < maxRef #the catalog i s not f u l l Variables # l o c a l to the s e r v i c e c : I n t e g e r ; # c : input code given by the user r e s : R e f e r e n c e ; d : S t r i n g ; # product d e s c r i p t i o n I n i t i a l i z a t i o n r e s := n o Q u a n t i t y ; Behavior I n i t i # the i n i t i a l state F i n a l f # a f i n a l state Context and message mappings.

END_COMPOSITION

In the next section, we show how this Kmelia specication is analysed using our COSTO 6 tool and a specic verication approach using the B method and tools.

Formal Analysis and Experimentations

Components, assemblies and compositions should be analysed according to various facets. Tables ?? and ?? give an overview of the verication requirements that we consider to validate a Kmelia specication. Some of them was achieved before, in particular the behavioural compatibility of services and components, treated in [?]:

it was achieved using model-checking techniques provided by existing tools (Lotos/-CADP 7 and MEC 8 ); the involved parts of the Kmelia specications were translated into the input languages these tools and checked.

In this section, we address aspects related to data type checking and assertion checking; the main goal is to analyse parts of a Kmelia specication using its new features such as the assertions.

Formal verication tools are necessary to check assertions consistency. Our approach consists in reusing existing tools such as the B tools and especially the Rodin 9 framework. We design a systematic verication method that enables us to reuse the proof obligations generated by the B tools for our specic purpose.

Analysis Status

experimental (i) eLTS (behaviour) compatibility [?] done Table 2 Formal analysis of a Kmelia assembly and compositions

Event-B and Rodin framework. Rodin is a framework made of several tools dedicated to the specication and proof of Event-B models. Event-B [?] extends the classical B method [?] with specic constructions and usage; it is intended to the modelling of general purpose systems and for reasoning on them. Proof obligations (POs) are generated to ensure the consistency of the considered model, i.e. the preservation of the INVARIANT by the EVENTS. Other POs ensure that a rened model is consistent, i.e. the abstract INVARIANT is preserved and the rened events do not contradict their abstract counterparts.

POs can be discharged automatically or interactively, using the Rodin provers.

Verifying Kmelia specications using Event-B. The main idea is, rst to consider a part of the Kmelia specication involved in the property to be veried (a service, a component, a link of an assembly, an assembly, etc), then to build from this part of the specication, a set of (Event-)B models in such a way that the POs generated for them correspond to the specic obligations we needed to check the Kmelia specication assertions. Using B to validate components assembly contracts has been investigated in [?,?].

We systematically build some Event-B models, with an appropriate structure as explained below, check some of the proof obligations presented in Tables ?? and ??. (ii) For each required service (and its virtual context) we have to generate an Event-B model. Its B consistency establishes the rule (c).

(iii) For each assembly link between a required service req and an provided one prov , we give an Event-B model of the observable part of prov, which renes the Event-B model of the required service req previously checked.

• the consistency proof of the Event-B model ensures the rule (a) for the in- variant consistency at the Kmelia level;

• the renement proof establishes both the rules (d) and (e) for the Kmelia assembly correctness.

We are not going to deal in this article with the details of the translation procedure. Kmelia invariant and pre-condition translations are quite systematic, whereas the post-condition concept does not exist into the B language. Therefore we abstract the post-condition by using an ANY substitution that satises the post-condition Experimental results. Consider the case study presented in Section ??; applying our method, we obtain the Event-B models structured as depicted in Fig ? ?.

These models are studied within Rodin.

We can verify the Kmelia components StockManager and Vendor before checking the assembly StockSystem. The Event-B model StockManager is used to prove the preservation of the invariant assertions by the provided services. The renement v_addItem_sm_newReference is used to check the assembly link between the services newReference and addItem. The Table ?? gives an idea about the number of POs that are to be discharged to ensure Fig. 3. Rodin the correctness of the Kmelia specication.

Studying the example within Rodin, reveals some errors in our initial Kmelia specication. For example, the post-condition of newReference was wrong; one of the associated POs could not be discharged. After the feedback in our Kmelia specications, the error was corrected.

Table 3 Rodin Proof obligations

In a general manner, the assertions associated to Kmelia services help us to ensure the correctness of the assembly link by considering the required-provided relationship as a renement from the required service to the provided one. When the assertions are wrong, the proofs fail, which means the assembly link is wrong.

In this article we have presented enrichments to the Kmelia abstract component model: a data language for Kmelia expressions and predicates; visibility features for component state in the context of composite components; contracts in the composition of services. The formal specication and analysis of the model are revisited accordingly. The syntactic analysis of Kmelia is eective in the COSTO tool that supports the Kmelia model. We have proposed a method to perform the necessary assertions verication using B tools: the contracts are checked through preliminary experimentations using the Rodin framework. We have illustrated the contribution with a complete case study which is specied in Kmelia and veried using Rodin.

Discussion. Our work is more related to abstract and formal component models like SOFA or Wright, rather than to the concrete models like Corba, EJB or .NET.

The Java/A [?] or ArchJava [?] models do not allow the use of contracts. We have already emphasized (see ??) the fact that most of the abstract models deal mainly with the dynamic part of the components. Some of them [?,?] take datatypes and contracts into account but not the dynamic aspects. Some other ones [?,?] delay the data part to the implementation level.

In [?] may/must constraints are associated to the interactions dened in the component interfaces to dene behavioural contracts between client and suppliers.

In Kmelia, the distinction between a supplier constraint and the client is done from a methodological point of view rather than a syntactic rule. The use of B to check component contracts has been studied in [?,?] in the context of UML components. Perspectives. Several aspects remain to deal with regarding assertions and the related properties, composition and correctness of component assemblies. First, we need to implement the full chain of assertion verication especially the translation KmlToB which is necessary to automatically derive the necessary Event-B models to check the assertions and the assemblies.

Second, we will integrate high level concepts and relations for data types. Especially we plan to integrate some kind of objects and inheritance in the type system but also component types. Assertions in this context are more dicult to specify and to verify.

Another challenging point is the support for interoperability with other component models. We assume that in real component applications, a component assembly is built on components written in various specication languages. When connecting services (or operations) we can at least check the matching of signatures. If the specication language of the corresponding services or components accepts contracts (resp. service composition, service behaviour) we can provide corresponding verication means.

A The Vendor Component Partial Specication # product re f e re n ce given by the user q t y : I n t e g e r ;

# product quantity given by the user d e s c : S t r i n g ;

# product d e s c r i p t i o n given by the user p i : I n t e g e r ;

Behavior // The behaviour i s s p e c i f i e d as an i n f i n i t e loop I n i t i # i i s the i n i t i a l state F i n a l f # f i s a f i n a l state

  c : C can be promoted as a variable vp ∈ V CP of a composite component cp : CP . Formally, there are a bijection prom : V O C → V CP which establishes the variable promotion, i.e. a bridge between the variable names. In the Kmelia syntax, (vo, vp) ∈ prom, is written vp FROM c.vo. The promoted variables retain their types (type(vp) = type(vo)) and are accessed (read-only at the composite level) in their eective contexts using a service of the sub-component that denes the variables.

Fig. 2 .

 2 Fig. 2. Simplied Assembly of the Stock Case Study

  v i d e s : { n e w R e f e r e n c e , r e m o v e R e f e r e n c e , s t o r e I t e m , o r d e r I t e m } r e q u i r e s : { a u t h o r i s a t i o n } USES {STOCKLIB} TYPES R e f e r e n c e : : range 1 . . maxRef VARIABLES v e n d o r C o d e s : setOf I n t e g e r ; // authorised administrators obs c a t a l o g : setOf R e f e r e n c e ; // product id = index of the arrays p l a b e l s : a r r a y [ R e f e r e n c e ] o f S t r i n g ; // product d e s c r i p t i o n p s t o c k : a r r a y [ R e f e r e n c e ] o f I n t e g e r // product quantity INVARIANT obs @borned : s i z e ( c a t a l o g ) <= maxRef , @ r e f e r e n c e d : f o r a l l r e f : R e f e r e n c e | inc lude s ( c a t a l o g , r e f ) i m p l i e s ( p l a b e l s [ r e f ] <> e m p t y S t r i n g and p s t o c k [ r e f ] <> n o Q u a n t i t y ) , @ n o t r e f e r e n c e d : f o r a l l r e f : R e f e r e n c e | excludes ( c a t a l o g , r e f ) i m p l i e s ( p l a b e l s [ r e f ] = e m p t y S t r i n g and p s t o c k [ r e f ] = n o Q u a n t i t y ) INITIALIZATION c a t a l o g := emptySet ; v e n d o r C o d e s := emptySet ;

  { i --c := __CALLER ! ! ask_code ( ) --> e1 , # gets the password on the ask_code ( s e r v i c e ) channel e1 --[ not ( c in v e n d o r C o d e s ) ] d i s p l a y ( " a d d i n g a r e f e r e n c e i s not a l l o w e d " ) --> end , e1 --[ c in v e n d o r C o d e s ] __CALLER ? msg ( d ) --> e2 , # gets the product d e s c r i p t i o n e2 --[ d = e m p t y S t r i n g ] d i s p l a y ( " a d d i n g an EmptySet d e s c r i p t i o n i s not a l l o w e d " ) --> end , e2 --[ d <> e m p t y S t r i n g ] r e s := __SELF ! ! g e t N e w R e f e r e n c e ( ) --> e4 , e4 --{ c a t a l o g := i n c l u d i n g ( c a t a l o g , r e s ) ; //add new re f er e nc e p s t o c k [ r e s ] := 0 ; // d ef au lt stock i s n u l l p l a b e l s [ r e s ] := d // product d e s c r i p t i o n i s the one provided }--> end , end --__CALLER ! ! n e w R e f e r e n c e ( r e s ) --> f # the c a l l e r i s informed from the Result and the s e r v i c e ends . } Post obs @ r e s u l t R a n g e : ( ( R e s u l t >= 1 and R e s u l t <= maxRef ) or ( R e s u l t = n o R e f e r e n c e ) ) , obs @ r e s u l t V a l u e : ( R e s u l t <> n o R e f e r e n c e ) i m p l i e s ( n o t I n ( o l d ( c a t a l o g ) , R e s u l t ) and c a t a l o g = add ( o l d ( c a t a l o g ) , R e s u l t ) ) , obs @ n o r e s u l t V a l u e : ( R e s u l t = n o R e f e r e n c e ) i m p l i e s Unchanged { c a t a l o g } , @ r e f A n d Q u a n t i t y : ( R e s u l t <> n o R e f e r e n c e ) i m p l i e s ( p s t o c k [ R e s u l t ] = 0 and p l a b e l s [ R e s u l t ] <> e m p t y S t r i n g and ( f o r a l l i : R e f e r e n c e | ( i <> R e s u l t ) i m p l i e s The behaviour of a service is a set of transitions. A transition is labelled and links two states like in e1 ---label---> e2. A transition label is a combination of actions.A label can be guarded with the notation [ guard] action * .The Kmelia syntax of a communication action (inspired by the Hoare's CSP) is: channel( ! | ? | !! | ? ? ) message(param * ). _CALLER stands for the caller channel, _SELF stands for an internal channel, _rs stands for a required service rs channel. In this article we will not consider further the behaviour. Nevertheless the actions are necessary to check the consistency of the behaviour with respect to the pre-/post-conditions.

  (i) For each component and its provided services, we generate an Event-B model.The proof of the consistency of this model ensures the proof of the rules (a) and (b) for the invariant consistency at the Kmelia level.

(

  once translated) as proposed in the context of UML/OCL to B translations [?].

Figure ?? depicts

  Figure ?? depicts the Event-B translation into Rodin of the service newReference of StockManager.

Fig. 4 .

 4 Fig. 4. Event-B Models

  Fractal [?] proposes dierent approaches based on the separation of concerns: the common structural features are dened in Fractal ADL [?] ; dynamic behaviours are implemented by Vercors [?] or Fractal/SOFA [?] and the use of assertions are studied in ConFract [?]. In ConFract contracts are independent entities which are associated to several participants, not to services and links as in our case; their contracts support a rely/guarantee mechanism with respect to the (vertical) composition of components.

Listing 4 :

 4 Kmelia specication Vendor COMPONENT Vendor INTERFACE p r o v i d e s : { v e n d i n g } r e q u i r e s : { a d d I t e m , r e m o v e I t e m , i n c r e a s e I t e m , d e c r e a s e I t e m } USES {STOCKLIB} CONSTANTS obs noID : I n t e g e r := -1 ; VARIABLES obs o r d e r s : setOf P r o d u c t I t e m ; # observable user card v e n d o r I d : I n t e g e r # vendor personal code INITIALIZATION o r d e r s := emptySet ; v e n d o r I d := noID SERVICES ########### provided s e r v i c e s # The main ( provided ) s e r v i c e i s vending . provided v e n d i n g ( ) I n t e r f a c e e x t r e q u i r e s : { a d d I t e m , r e m o v e I t e m , i n c r e a s e I t e m , d e c r e a s e I t e m } Pre t r u e Variables # l o c a l to the s e r v i c e c h o i c e : CommandChoice ; # command choice : addItem , . . . r e f : I n t e g e r ;

: 3 END:::

 3 { i --{ d i s p l a y M e n u ( ) ; # c a l l an i n t e r n a l action d i s p l a y ( " P l e a s e e n t e r y o u r c h o i c e " ) ; c h o i c e := readCommandChoice ( ) # c a l l an i n t e r n a l action } --> e0 , e0 --[ c h o i c e = s t o p ] d i s p l a y ( " bye bye " ) --> f , // f i n a l state = end of vending e2 --[ c h o i c e = add ] _addItem ! ! a d d I t e m ( ) --> e10 , e0 --[ c h o i c e <> s t o p ] d i s p l a y ( " P r o d u c t r e f e r e n c e " ) --> e1 , References = 1 . . MaxRef axm1 : MaxRef = 100 axm2 : NullInt = -1 axm3 : NoQuantity = -2 axm4 : NoReference = -vendorCodes ⊆ Z inv2 : catalog ∈ P(References) obs inv7 : finite(catalog)obs inv3 : plabels ∈ 1 . . MaxRef → String inv4 : pstock ∈ 1 . . MaxRef → Z • borned : card(catalog) ≤ MaxRef obs • referenced : ∀ref1 •(ref1 ∈ References ∧ ref1 ∈ catalog⇒plabels(ref1 ) = EmptyString ∧ pstock (ref1 ) = NoQuantity) • notreferenced : ∀ref2 •(ref2 ∈ References ∧ ref2 / ∈ catalog⇒plabels(ref2 ) = EmptyString ∧ pstock (ref2 ) = NoQuantity) inv6 : Result newReference ∈ Z obs EVENTSInitialisation begin act1 : vendorCodes := ∅ act2 : catalog := ∅ act3 : plabels := (1 . . MaxRef ) × {EmptyString} act4 : pstock := (1 . . MaxRef ) × {NoQuantity} act5 : Result newReference :card(catalog) < MaxRef obs grd1 : new Result ∈ Z obs grd2 : new catalog ∈ P(References) obs grd11 : finite(new catalog) obs grd3 : new plabels ∈ 1 . . MaxRef → String grd4 : new pstock ∈ 1 . . MaxRef → Z grd5 : (new Result > 0 ∧ new Result ≤ MaxRef ) ∨ new Result = NoReference obs grd6 : new Result = NoReference ⇒ new Result / ∈ catalog ∧ new catalog = catalog ∪ {new Result}obs grd7 : new Result = NoReference ⇒ new catalog = catalog obs grd9 : new Result = NoReference ⇒ new pstock(new Result) = 0 ∧ new plabels(new Result) = EmptyString ∧ (∀ii •(ii ∈ 1 . . MaxRef ∧ ii = new Result ⇒ new pstock (ii) = pstock (ii) ∧ new plabels(ii) = plabels(ii) )) grd10 : new Result = NoReference ⇒ new pstock = pstock ∧ new plabels = plabelsthen act1 : Result newReference := new Result act2 : catalog := new catalog act3 : pstock := new pstock act4 : plabels := new plabels catalogFull ∈ BOOL inv2 : catalogEmpty ∈ BOOL • notFullEmpty : ¬ (catalogEmpty = TRUE ∧ catalogFull = TRUE ) inv4 : Result addItem ∈ Z EVENTS Initialisation begin act1 : catalogFull := FALSE act2 : catalogEmpty := TRUE act3 : Result addItem :∈ Z end Event addItem = any new Result new catalogEmpty new catalogFull where pre addItem : ¬ (catalogFull = TRUE ) grd2 : new Result ∈ Z grd6 : new catalogEmpty ∈ BOOL grd5 : new catalogFull ∈ BOOL Post addItem : new Result = NoReference ⇒ new catalogEmpty = FALSE ∧ new catalogFull ∈ BOOL Post addItem2 : new Result = NoReference ⇒ new catalogEmpty = catalogEmpty ∧ new catalogFull = catalogFull then

  Observability rules vs. service state space. Let s be a service of a component type C. The distinction between observable and non-observable variables of the component state space is revisited 3 according to the following table:

	Service	Variables	Invariant
	state space	Observable part Non-observable part	Observable part Non-observable part
	Provided s

  5 and the ask_code service Andre et al. required to its caller.Data types in Kmelia. The data types are explicitly dened in a TYPES clause or in the shared libraries (predened or user-dened). As an example, the following library (named Stocklib ) declares some specic types, functions and constants. TYPES P r o d u c t I t e m : : s t r u c t { i d : I n t e g e r ; d e s c : S t r i n g ; q u a n t i t y : I n t e g e r } ;This data types in this part are quite concrete; more abstract data types are in the process to be included in the predened library.A Kmelia component and observable state. The listing ?? is an extract from the Kmelia specication of the StockManager component. The state of StockManager declares among the other variables, the observable variable catalog which can be used for context mapping in the assembly links but also in promoted variables for composite components. Two arrays ( plabels and pstock) are used to stock the labels of current references and their available quantity. The invariant states that: the catalog has an upper bound; all references in the catalog have a label and a quantity; the unknown references have no entries in the two arrays pstock and plabels . The assertions in Kmelia are possibly named predicates; the labels in front of the invariant lines are names used in this specication.

	CONSTANTS maxRef : I n t e g e r := 100 ; e m p t y S t r i n g : S t r i n g := "" ; n o R e f e r e n c e : I n t e g e r := -1 ; n o Q u a n t i t y : I n t e g e r := -1

Listing 1: Kmelia specication StockManager State

  The context and message mappings (see ??) are specied in assembly links. In the listing ??, variables of the virtual context of addItem are associated with an expression on the variables of the context of newReference i.e. the observable state variables of the component sm. In this example, there are no message mapping because only the predened overloaded msg == empty ( sm . c a t a l o g ) , ve . c a t a l o g F u l l == s i z e ( sm . c a t a l o g ) = MaxInt s u b l i n k s : { l c o d e } l c o d e : r-p sm . ask_code , ve . code

	r e q u i r e s : { a u t h o r i s a t i o n }
	SERVICES
	END_SERVICES
	COMPOSITION
	Assembly
	Components
	sm : StockManager ;
	ve : Vendor
	Links //////////// assembly l i n k s //////////
	l r e f : p-r sm . n e w R e f e r e n c e , ve . a d d I t e m
	c o n t e x t mapping
	ve . c a t a l o g E m p t y . . .
	message is used.
	Listing 3: Kmelia specication StockSystem
	COMPONENT S t o c k S y s t e m
	INTERFACE
	p r o v i d e s : { v e n d i n g }

End // assembly Promotion Links //////////// promotion l i n k s ////////// l v e n d : p-p ve . v e n d i n g , SELF . v e n d i n g l a u t : r-r sm . a u t h o r i s a t i o n , SELF . a u t h o r i s a t i o n

  Inv O ∧ P re O ⇒ P ost O ∧ Inv O experimental (a) P ost the post condition should be established required service R calls vs. P re R the context must ensure the precondition (local+virtual) eLTS vs. subprovided service SP annotations P re SP the context must ensure the precondition (local)

	Static rules: Scope + name resolution + type-checking	done
	Observability rules (see ??)	in progress
	Component interface consistency	done
	Services dependency consistency:
	DI well-formed vs. I and D (component)	done
	DI vs. B (eLTS)
	Simple constraint checking (parameters, query, protocol, . . . )	in progress
	Local eLTS checking (deadlocks, guard, subprovides, . . . )	in progress
	Invariant consistency vs. pre/post conditions:
	provided services : Inv ∧ P re ⇒ P ost N O ∧ Inv	experimental (b)
	required services : vInv ∧ P re O ⇒ P ost O ∧ vInv	experimental (c)
	Consistency between service assertions and eLTS:	not yet
	eLTS vs. Table 1 Formal analysis of a simple Kmelia component
	Analysis	State
	Static rules: Scope + name resolution + type-checking	done
	Observability rules: promoted variables	done
	Link/sublink consistency: assembly and composition	done
	signature matching
	service dependency matching (subprovides, callrequires)
	context mapping (cm function) and observability rules
	message mapping
	Assembly Link Contract correctness:
	cm(P re O R ) ⇒ P re O P	experimental (d)
	P ost O P ⇒ cm(P ost O R )	experimental (e)
	Provided Promotion Link Contract correctness: PP is at the composite level
	cm(P re O P P ) ⇒ P re O P	experimental (f)
	P ost O P ⇒ cm(P ost O P P )	experimental (g)
	Required Promotion Link Contract correctness: RR is at the composite level
	cm(P re O R ) ⇒ P re O RR	experimental (h)
	P ost O RR ⇒ cm(P ost O R )

and by extension a service of a component c : C

In Kmelia, a subservice of a service s, is a service that belongs to the interface (subprovides) of s.

which is also a subservice because it is not exposed in the StockManager component interface

COmponent Sudy TOolkit dedicated to the Kmelia language

http://www.inrialpes.fr/vasy/cadp/

http://altarica.labri.fr/wiki/tools:mec_4

http://rodin-b-sharp.sourceforge.net