Verification of Software Components

Organisation:	University of Nantes (FRANCE)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems.
Period:	2006
Size:	About 540 lines of LOTOS
Description:	The rigorous development of large systems based on software components is still a challenging research topic. In this context, composition is a central issue. Thus, composing components is source of errors, and can easily insert deadlocks within a system. Hence, formal models are necessary to describe component interfaces and compositions. In a second step, validation and verification tools can be used to ensure correct interactions between the involved entities. This case-study presents a tool-equipped approach to design component-based systems using an architecture description language abstract Kmélia. This language allows to specify the hierarchical composition between services and components, the main ingredient being the notion of service composition. Each service is equipped with an interface indicating the subservices offered and required in view of the decomposition of the service and its connection with other services. The behaviour of services is described in terms of extended labelled transition systems involving data values and guarded transitions. From descriptions of the component interfaces and compositions, CADP is used to check that components involved in a composition can interact as required and reach a correct termination state. The properties of interest are described in the regular alternation free mu-calculus and successfully verified with the EVALUATOR model-checker of CADP. The verification step is possible thanks to a prototype translator which generates automatically LOTOS specifications corresponding to the abstract descriptions of the components and their interactions.
Conclusions:	This case-study shows that LOTOS is adequate as a target language to describe automata-based descriptions of software components. CADP was used in a second step to check their correct composition. At this level, several errors were found out, for instance some impossible communications were detected and then corrected.
Publications:	[Attiogbe-Ardourel-Andre-06] Christian Attiogbé, Gilles Ardourel, and Pascal André. "Checking Component Composability". In Welf Lowe and Mario Sudholt (editors), Proceedings of the 5th International Symposium on Software Composition SC'06 (Vienna, Austria), Lecture Notes in Computer Science, vol. 4089, pp. 18-33, Springer Verlag, March 2006. Available from the CADP Web site in PDF or PostScript [Andre-Ardourel-Attiogbe-06] Pascal André, Gilles Ardourel, and Christian Attiogbé. "Spécification d'architectures logicielles en Kmélia: hiérarchie de connexion et composition". In Flavio Oquendo and Mourad Oussalah (editors), 1ère Conférence Francophone sur les Architectures Logicielles CAL'06 (Nantes, France), Hermès Science/Lavoisier, Septembre 2006. Available from the CADP Web site in PDF or PostScript
Contact:	Christian Attiogbé LINA - Faculté des sciences 2, rue de la Houssinière BP 92298 F-44322 Nantes Cedex 3 FRANCE Tel.: +33 (0)2 51 12 58 18 E-mail: Christian.Attiobge@univ-nantes.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page