Database of Research Tools Developed Using CADP

COSTO Tool for Analyzing Kmelia Components and Services

Organisation: Université de Nantes (FRANCE)

Functionality: Model checking for component-based systems.

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2008 - 2010

Description: The modelling of various real life systems (e.g., auction systems, chat systems, distributed brokers, etc.) requires the use of several components of the same type or several services with identical functionalities but coming from different components. The design of such systems needs the ability to describe the assembly and the composition w.r.t. the multiplicity of services that may be connected. The Kmelia abstract component model was introduced to support the specification and development of correct components. The model is equipped with a language allowing the description of components and services. Two different semantics are defined for linking component services: monadic semantics (only one provided service may be associated to a requested service) and polyadic semantics (a provided service may be linked with various required services).

Kmelia allows to define components and assemblies (sets of components linked through their services). A Kmelia abstract component is a mathematical model of an open multiservice system that supports synchronous communication with its environment. The polyadic semantics is defined by means of shared services and multipart communications. Well-formed Kmelia specifications must satisfy the properties of composability and behavioural compatibility.

Formal analysis for Kmelia is supported by the COSTO toolbox, which is able to parse Kmelia specifications, translate them into LOTOS, and check service properties (including behavioural compatibility) using CADP. The negotiated multiway rendezvous of LOTOS is useful for modelling the multipart communications between Kmelia components. The usage of Kmelia and COSTO is illustrated on a chat system with shared services.

Conclusions: Process algebraic languages like LOTOS are naturally adapted to the description of concurrency, and can serve as target languages for translating component-based description languages like Kmelia. A direct benefit of such translations is the direct access to the formal analysis functionalities provided by tools like CADP. Further work on Kmelia includes the study of sharing and related properties, composition and correctness of component assemblies, and also the suport for interoperability with other component models.

Publications: [Andre-Ardourel-Attiogbe-08] Pascal André, Gilles Ardourel, Christian Attiogbé. "Composing Components with Shared Services in the Kmelia Model". In Cesare Pautasso and Eric Tanter, editors, Proceedings of the 7th International Symposium on Software Composition SC'2008 (Budapest, Hungary), Lecture Notes in Computer Science, volume 4954, pp. 125-140, March 2008.
Full version available from our FTP site in PDF or PostScript

[Andre-Ardourel-Attiogbe-Lanoix-10] Pascal André, Gilles Ardourel, Christian Attiogbé and Arnoud Lanoix. "Using Assertions to Enhance the Correctness of Kmelia Components and their Assemblies". In Electronic Notes in Theoretical Computer Science 263 (2010) 5-30.
Available on line from
or from our FTP site at PDF or PostScript

[Messabihi-Andre-Attiogbe-10] Mohamed Messabihi, Pascal André, and Christian Attiogbé. "Multilevel Contracts for Trusted Components". Proceedings of the International Workshop on Component and Service Interoperability (WCSI'10), EPTCS vol. 37, pp. 71-85, 2010.
Available on line from
or from our FTP site at PDF or PostScript
Pascal André
2, rue de la Houssinière
B.P. 92208
44072 Nantes Cedex 03
Tel: 02 51 12 59 65
Fax: 02 51 12 58 12

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:13:01 2016.

Back to the CADP research tools page