Formal Analysis of Choreography Specifications

Organisation:	Inria Grenoble - Rhône-Alpes (FRANCE) University of Nantes (FRANCE) University of California at Santa Barbara (USA) Sharif University of Technology (IRAN)
Functionality:	Formal analysis of choreographies.
Tools used:	Python CADP (Construction and Analysis of Distributed Processes)
Period:	2012
Description:	Many software systems are now built using independently developed services, which are mostly geographically and organizationally distributed. The specification and analysis of interactions among such distributed systems is a major concern for ensuring their correctness and reliability. In order to simplify the construction of these systems, their design often relies on a contract, which describes from a global point of view the admissible interaction sequences exchanged between the participants. In the area of Service Oriented Computing (SOC), this contract is called choreography and the participants are called peers. The peers correspond to a distributed implementation of this choreography, and can be derived by projection, i.e., by projecting the choreography specification to each peer by ignoring the messages that are not sent or received by that peer. A crucial question in this context is to check whether the peers behave exactly as required in the choreography. This property is called realizability and particularly matters when the system is built following a top-down development process. Choreographies can be specified using specification languages such as Web Services Choreography Description Language (WS-CDL) and visualized using graphical formalisms such as collaboration diagrams. This work proposes an encoding of collaboration diagrams into the LOTOS process algebraic language for choreography analysis. LOTOS provides the necessary level of expressiveness to describe all the collaboration diagram interaction constraints and is equipped with the state-of-the-art state space exploration and verification functionalities of the CADP toolbox. This encoding allows the designer to (i) check the temporal properties of choreographies using CADP, (ii) check the realizability of choreographies for both synchronous communication and bounded asynchronous communication, and (iii) automate the peer generation process. Realizability indicates whether peers can be generated from a given choreography specification in such a way that the interactions of the generated peers exactly match the choreography specification. When a choreography is not realizable, a new approach is proposed, which identifies all (message ordering) problems which prevent realizability of a choreography, and provides a possible solution to enforce them. This is done by automatically generating monitors, which act as local controllers interacting with their peer and the rest of the system in order to make the peers respect the choreography requirements. These monitors are obtained by first generating the set of distributed peers by projection from the choreography specification. Then, the system synchronizability (i.e., the system behavior, considering the send messages, preserves the same message sequences under synchronous and 1-bounded asynchronous communication) and realizability properties are verified using equivalence checking. If one of these properties is violated, the generated counterexample is exploited to augment the monitors with a new synchronization message. Monitors are obtained through an iterative process, automatically refining their behaviors. The successive addition of these messages will finally enforce both synchronizability and realizability. This approach has been automated by encoding choreographies into the value-passing process algebra LNT, one of the input languages of CADP. This makes possible the reuse of existing state space exploration tools for generating peers and distributed systems, and equivalence checking techniques for verifying synchronizability and realizability. The process is fully supported (no human intervention) by calling various tools, some reused from CADP, others newly implemented (e.g., for automating the iterative part of the process). The approach has been validated on hundreds of examples, some of them borrowed from real-world scenarios found in the literature.
Conclusions:	The proposed framework for modeling and analyzing choreographies, based on value-passing process algebras and the CADP toolbox, is directly applicable to all notations which are transformable into conversation protocols (e.g., BPMN 2.0, collaboration diagrams, WS-CDL, Singularity channels, MSC, etc.).
Publications:	[Salaun-Bultan-Roohi-12] Gwen Salaün, Tevfik Bultan, and Nima Roohi. "Realizability of Choreographies Using Process Algebra Encodings". IEEE Transactions on Services Computing 5(3):290-304, 2012. Available on-line at: http://hal.inria.fr/hal-00726448/en or from the CADP Web site in PDF or PostScript [Gudemann-Salaun-Ouederni-12] Matthias Güdemann, Gwen Salaün, and Meriem Ouederni. "Counterexample Guided Synthesis of Monitors for Realizability Enforcement". Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis ATVA'2012 (Thiruvananthapuram, India), Lecture Notes in Computer Science vol. 7561, pages 238-253. Springer Verlag, October 2012. Available on-line at: http://hal.inria.fr/hal-00742159/en or from the CADP Web site in PDF or PostScript [Poizat-Salaun-12] Pascal Poizat and Gwen Salaün. "Checking the Realizability of BPMN 2.0 Choreographies". Proceedings of the 27th Symposium on Applied Computing SAC'2012 (Riva del Garda, Italy), pages 1927-1934. ACM Computer Society Press, March 2012. Available on-line at: http://hal.inria.fr/hal-00685393/en or from the CADP Web site in PDF or PostScript [Dumont-12] Alexandre Dumont. "A LOTOS NT Library for Modelisation, Analysis, and Validation of Distributed Systems". Internship Report, Ecole Nationale Supérieure d'Informatique et Mathématiques Appliquées de Grenoble (ENSIMAG), June 2012. Available on-line at: http://ensiwiki.ensimag.fr/images/1/15/Alexandre-dumont-rapport.pdf or from the CADP Web site in PDF or PostScript
Contact:	Gwen Salaün Inria Grenoble - Rhône-Alpes CONVECS team 655, avenue de l'Europe F-38330 Montbonnot Saint Martin France Tel: +33 (0)4 76 61 54 28 Fax: +33 (0)4 76 61 52 52 Email: Gwen.Salaun@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