System-on-Chip Laboratory (LabSoC), Telecom Paristech
INRIA, CNRS, I3S, University of Nice Sophia-Antipolis
(Sophia Antipolis, FRANCE)
CADP (Construction and Analysis of Distributed Processes)
13,327,161 states and 48,569,764 transitions
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.
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
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.
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 our FTP 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 our FTP site in PDF or PostScript
INRIA Sophia Antipolis
2004, Route des Lucioles
F-06902 Sophia-Antipolis Cedex
Tel: +33 4 92 38 71 64
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|