Verification of the Behavioural Properties for Group Communications

Organisation:	System-on-Chip Laboratory (LabSoC), Telecom Paristech and INRIA, CNRS, I3S, University of Nice Sophia-Antipolis (Sophia Antipolis, FRANCE)
Method:	pNets FIACRE LOTOS LTS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Distributed Systems.
Period:	2010
Size:	13,327,161 states and 48,569,764 transitions
Description:	The group communication approach enables a groups of distant objects to be viewed locally as a single object, greatly simplifying interactions between the local application and the remote objects. Objects can join and leave the group without the need to notify the application. A communication sent to the group object is conveyed to all objects belonging to the group according to the distribution policy (broadcast, forwarding, etc.). There are several middleware platforms for creating distributed applications that implement this one-to-many communication mechanism. This case study addresses the issue of reliability of distributed applications using group communications, including notably the ability of the application to detect deadlocks. The behaviour of complex systems can be represented hierarchically by composition of classical Labelled Transition Systems (LTSs). Those LTSs are composed using synchronisation Networks (Net) so that the synchronisation product generates a LTS which can be used at the higher level of the hierarchy. Finally the behavior of the system can be expressed by a global LTS. Using the ProActive middleware as typical example of middleware offering a group communication mechanism, the case study considers an application for scheduling meetings, with a meeting Initiator and several clients, each containing a participant's calendar. The Initiator sends communications to the Participant clients as a group. The system specification was written in FIACRE, and the state space was generated on a cluster of 15 8-core nodes using the DISTRIBUTOR tool of CADP. Behavioural properties were expressed using regular alternation-free mu-calculus and the specification patterns library provided by CADP, and were verified using the EVALUATOR model checker. Additionally, the behaviour of the LOTOS representation generated from the FIACRE code was explored using the OCIS graphical simulator, and the diagnostics generated by the model checker were checked visually using BCG_EDIT.
Conclusions:	Group communication is a convenient mechanism for one-to-many communication within a distributed application, so it is vital that such communication be reliable. This case study outlined a method for verifying the correct behaviour of such applications. Though it focussed only the ProActive middleware, there is no reason why this method could not be applied to other middleware frameworks, because the parameterized models are supported by model checking tools and are hierarchical LTSs, which can be analysed by verification tools based on bisimulation. The VERCORS tool platform used in conjunction with CADP to handle this case study is presented in http://cadp.inria.fr/software/06-e-vercors.html Group-based distributed systems typically have large, though finite, state spaces so the on-the-fly model checking tools of CADP and the DISTRIBUTOR tool are necessary because they avoid the need to generate the entire state space. Future work to automate the translation from pNet to FIACRE would enhance the usability of this approach.
Publications:	[Boulifa-Henrio-Madelaine-10] Rabéa Ameur-Boulifa, Ludovic Henrio, and Eric Madelaine. "Behavioural models for group communications". Proceedings of the International Workshop on Component and Service Interoperability WCSI'10 (Malaga, Spain), Electronic Proceedings in Theoretical Computer Science (EPTCS) vol. 37, pages 42-56, 2010. Available on-line at: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.170.515 or from the CADP Web site in PDF or PostScript [Henrio-Madelaine-10] Ludovic Henrio and Eric Madelaine. "Experiments with Distributed Model-Checking of Group-Based Applications". Proceedings of the Sophia-Antipolis Formal Analysis Workshop, INRIA/CNRS, November 2010. Available on-line at: http://hal.inria.fr/inria-00538499 or from the CADP Web site in PDF or PostScript
Contact:	Ludovic Henrio INRIA Sophia Antipolis 2004, Route des Lucioles BP 93 F-06902 Sophia-Antipolis Cedex FRANCE Tel: +33 4 92 38 71 64 Email: Ludovic.Henrio@sophia.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