VERCORS Platform for Model Checking Distributed Components

Organisation:	INRIA Sophia-Antipolis (FRANCE) and Univ. Diego Portales, Santiago (CHILE)
Functionality:	Model Checking.
Tools used:	FC2Tools CADP (Construction and Analysis of Distributed Processes)
Period:	2006-2010
Description:	Component programming consists in splitting the system into smaller and independent pieces of software that interact through well-defined interfaces. The Fractal distributed component model, implemented in Java, allows to design a system hierarchically by assembling individual components into more complex components, called composites. Although Fractal ensures the static compatibility between the interfaces of connected components, this does not suffice in general to prevent dynamic mismatches, such as deadlocks, caused by the behavioural uncompatibility of the components. In order to identify and fix such dynamic mismatches, it is necessary to build a formal model of components' behaviour, on which verification tools can be applied. The Vercors platform aims at providing a semi-automatic verification environment for distributed hierarchical components, by constructing a model from a system description and analyzing it using the CADP toolbox. Vercors takes as input the architecture of the system, specified in the Fractal Architecture Description Language (ADL), together with the functional behaviours of the primitive components, specified in LOTOS. To obtain models of tractable size, the user must provide finite abstractions for the (possibly infinite) data domains of the various parameters occurring in the system: the objects manipulated by the components, the values transmitted along communication channels, and the topology of component interconnection. The ADL description of the system architecture is processed by the ADL2N tool, which analyzes and translates it into a hierarchical synchronization network in the Parameterized FC2 format (pNet). ADL2N allows the user to hide the method calls that need not be observable during the subsequent analysis. The pNet, which contains parameterized actions, is then instantiated using the FC2Instantiate tool into a network of communicating automata in plain FC2 format. The FC2EXP tool translates this network into the EXP format accepted as input by the EXP.OPEN tool of CADP. The LOTOS specifications of the primitive components are compiled into labelled transition systems (LTSs) using the CAESAR tool of CADP. Finally, the LTS of the whole system is constructed with EXP.OPEN and analyzed using the verification tools of CADP. The functioning of the Vercors platform is illustrated on a realistic case-study implemented in Fractal and provided by France Telecom, namely a Wifi Internet access system available in airports. The system consists of a firewall responsible for the authentication of users based upon plane ticket numbers or frequent flyer IDs, and an arbitrator that implements the access policy. The Vercors platform and CADP allowed to build the LTS of the system (2,152 states and 6,553 transitions) and to detect a deadlock, which would have been difficult to identify without verification tools. The fact that any user cannot eventually get Internet access (because of repeated invalid authentication attempts) was also checked and diagnosed using the EVALUATOR model checker of CADP.
Conclusion:	The Vercors platform represents an attempt of integrating formal verification into the development of distributed, hierarchical component systems. The connection with a mature verification toolbox such as CADP allowed to focus the efforts on constructing formal models from Fractal architectural descriptions. The Vercors platform relieves the end-user from the burden of manipulating complex intermediate models and provides, through the use of CADP, useful diagnostics for non-trivial design flaws. Future work on the ADL2N tool will address component deployment and reconfiguration, as well as asynchronous communication.
References:	[Barros-Cansado-Madelaine-Rivera-06] Tomas Barros, Antonio Cansado, Eric Madelaine, and Marcela Rivera. "Model-Checking Distributed Components: The Vercors Platform". Proceedings of the 3rd International Workshop on Formal Aspects of Component Software FACS'2006, ENTCS vol. 182, pages 3-16, September 2006. Available on-line at: https://hal.inria.fr/inria-00091569/en or from the CADP Web site in PDF or PostScript [Cansado-Madelaine-09] Antonio Cansado and Eric Madelaine "Specification and Verification for Grid Component-Based Applications: From Models to Tools". Proceedings of the 7th International Symposium on Formal Methods for Components and Objects FMCO'2008, Lecture Notes in Computer Science vol. 5751, pages 180-203. Springer Verlag, August 2009. Available on line at: http://portal.acm.org/citation.cfm?id=1616470 or from the CADP Web site in PDF or PostScript [Barros-Boulifa-Cansado-et-al-09] Tomas Barros, Rabea Ameur-Boulifa, Antonio Cansado, Ludovic Henrio, and Eric Madelaine. "Behavioural Models for Distributed Fractal Components". Annals of Telecommunications 64(1-2):25-43, Springer Verlag, February 2009. Available on line at: http://www.springerlink.com/content/y4600803qr453774/ or from the CADP Web site in PDF or PostScript [Cansado-Henrio-Madelaine-et-al-10] Antonio Cansado, Ludovic Henrio, Eric Madelaine, and Pablo Valenzuela. "Unifying Architectural and Behavioural Specifications of Distributed Components". Electronic Notes in Theoretical Computer Science vol. 260, pages 25-45. Elsevier, 2010. Available on line at: http://www.sciencedirect.com/science/article/pii/S157106610900512X [Henrio-Madelaine-13] Ludovic Henrio and Eric Madelaine. "Behavioural Verification of Distributed Components". Proceedings of the 6th Interaction and Concurrency Experience (ICE'2013), Florence, Italy, June 2013. Available on line at: http://www.cs.unibo.it/~lanese/ice2013-papers/Henrio-Madelaine.pdf or from the CADP Web site in PDF or PostScript [Henrio-Kulankhina-Liu-Madelaine-14] Ludovic Henrio, Oleksandra Kulankhina, Dongqian Liu, and Eric Madelaine. "Verifying the Correct Composition of Distributed Components: Formalisation and Tool". Proceedings of the 13th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA'2014) Rome, Italy, September 2014. Available on line at: http://hal.inria.fr/hal-01055370/en or from the CADP Web site in PDF or PostScript [Henrio-Kulankhina-Li-Madelaine-15] Ludovic Henrio, Oleksandra Kulankhina, Siqi Li, and Eric Madelaine. "Integrated environment for verifying and running distributed components". INRIA Research Report 8841, December, 2015. Available on line at: http://hal.inria.fr/hal-01252323/en or from the CADP Web site in PDF or PostScript [Henrio-Kulankhina-Li-Madelaine-16] Ludovic Henrio, Oleksandra Kulankhina, Siqi Li, and Eric Madelaine. "Integrated Environment for Verifying and Running Distributed Components". Proceedings of the 19th International Conference on Fundamental Approaches to Software Engineering FASE'2016, Lecture Notes in Computer Science vol. 9633, pages 66-83. Springer Verlag, April 2016. Available on line at: http://link.springer.com/chapter/10.1007/978-3-662-49665-7_5 [Kulankhina-16] Oleksandra Kulankhina. "A Framework for Rigorous Development of Distributed Components: Formalisation and Tools". PhD Thesis, Université Nice Sophia-Antipolis, October 2016. Available on line at: http://www-sop.inria.fr/members/Oleksandra.Kulankhina/Oleksandra_thesis.pdf or from the CADP Web site in PDF or PostScript [AmeurBoulifa-Henrio-Kulankhina-et-al-17] Rabéa Ameur-Boulifa, Ludovic Henrio, Oleksandra Kulankhina, Eric Madelaine, and Alexandra Savu. "Behavioural Semantics for Asynchronous Components". Journal of Logical and Algebraic Methods in Programming 89:1-40, 2017. Available on line at: https://hal.inria.fr/hal-01526055/en or from the CADP Web site in PDF or PostScript See also http://cadp.inria.fr/case-studies/10-e-behaviour.html for a case study using Vercors and CADP.
Contact:	Eric Madelaine INRIA Sophia-Antipolis 2004, route des Lucioles BP 93 F-06902 Sophia-Antipolis FRANCE Tel: +33 (0)4 92 38 78 07 Fax: +33 (0)4 92 38 76 44 E-mail: Eric.Madelaine@sophia.inria.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