Verification of Fractal Components

Organisation:	INRIA Sophia Antipolis (FRANCE) University of Westminster (UNITED KINGDOM)
Method:	Parameterized networks of communicating automata ACTL (Action-based Computation Tree Logic) regular alternation-free mu-calculus
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems.
Period:	2005
Size:	Up to 191,000,000 states and 1,498,000,000 transitions
Description:	A software component is a self-contained entity, which inherits concepts from modules and objects to enforce structuring of applications. A component interacts with other components through well-defined interfaces. Fractal is a model of distributed components that can be composed together hierarchically to create new components, called composite. Fractal provides means for architecture and deployment descriptions, including non-functional features for controlling the life-cycle of components. This case-study presents a method and a tool intended to application developpers, to build behavioural models of Fractal components on which properties can be verified using CADP. The model of a non-composite component is obtained either from automatic analysis of source code, or expressed in a specification language. Non-functional behaviour is automatically incorporated within a controller built from the component's description. The behavioural model of a composite is then computed as a product of the labeled transition systems of its sub-components with the controller of the composition. The properties of interest are described either in ACTL (Action-based Computation Tree Logic), or in the regular alternation free mu-calculus. They include both non-functional properties such as effective start of all components in the hierarchy of components during deployment, and functional properties, such as request followed by response. The functional properties are also verified in the case when a component can be reconfigured during its execution.
Conclusions:	This case-study uses the CADP tools intensively. CADP allowed to generate both large state spaces (up to 191,000,000 states and 1,498,000,000 transitions generated using the distributed generation tool on a cluster of 24 bi-processor nodes in a first approach) and reduced state spaces on which all properties of interest could be verified in a simple desktop machine using compositional and on-the-fly verification.
Publications:	[Barros-Henrio-Madelaine-05-a] T. Barros, L. Henrio, and E. Madelaine. "Behavioural Models for Hierarchical Components". In Patrice Godefroid (editor), Proceedings of the 12th International SPIN Workshop on Model Checking of Software SPIN'2005 (San Francisco, USA), Lecture Notes in Computer Science, vol. 3639, pp. 154-168, Springer Verlag, August 2005. Available on-line at: http://www-sop.inria.fr/oasis/Vercors/papers/BehavModelsComponents.pdf or from the CADP Web site in PDF or PostScript [Barros-Henrio-Madelaine-05-b] T. Barros, L. Henrio, and E. Madelaine. "Verification of Distributed Hierarchical Components". In Proceedings of the International Workshop on Formal Aspects of Component Software FACS'05 (Macao), Electronic Notes in Theoretical Computer Science, October 2005. Available on-line at: http://www-sop.inria.fr/oasis/Vercors/papers/BehavModelsDistributedComponents.pdf or from the CADP Web site in PDF or PostScript
Contact:	Eric Madelaine INRIA Sophia Antipolis 2004, route des Lucioles BP 93 F-06902 Sophia Antipolis Cedex FRANCE Tel.: +33 (0)4 92 38 78 07 E-mail: Eric.Madelaine@inria.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