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 the CADP Web 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 at: http://hal.archives-ouvertes.fr/hal-00423672/en or from the CADP Web site in 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 at: http://arxiv.org/pdf/1010.2827v1 or from the CADP Web site in PDF or PostScript [Messabihi-11] Mohamed El-Habib Messabihi. "Contribution à la spécification et à la vérification des logiciels à base de composants : enrichissement du langage de données de Kmelia et vérification de contrats". PhD thesis, Université de Nantes, France, July 2011. Available on line at: https://hal.inria.fr/tel-01146895/document or from the CADP Web site in PDF or PostScript [Andre-Attiogbe-Mottu-17] Pascal André, Christian Attiogbé, and Jean-Marie Mottu. "Combining Techniques to Verify Service-based Components". Proceedings of the 5th International Conference on Model-Driven Engineering and Software Development MODELSWARD'2017 (Porto, Portugal), pages 645-656, SciTePress, February 2017. Available on line at: https://hal.archives-ouvertes.fr/hal-01628303/en or from the CADP Web site in PDF or PostScript [Andre-Cardin-17] Pascal André and Olivier Cardin. "Trusted Services for Cyber Manufacturing Systems". Proceedings of Service Orientation in Holonic and Multi-Agent Manufacturing (SOHOMA 2017), Studies in Computational Intelligence, vol 762, pages 359-370, October 2017. Available on line at: https://doi.org/10.1007/978-3-319-73751-5_27 or from the CADP Web site in PDF or PostScript
Contact:	Pascal André LINA 2, rue de la Houssinière B.P. 92208 44072 Nantes Cedex 03 France Tel: 02 51 12 59 65 Fax: 02 51 12 58 12 Email: Pascal.Andre@univ-nantes.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page