Skip to Main content Skip to Navigation
New interface
Conference papers

Experiments with distributed Model-Checking of group-based applications

Ludovic Henrio 1 Eric Madelaine 1 
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Group-based distributed systems are specific cases of distributed applications with a parameterized topology. They are naturally modelled by systems with a very large state space. We encode the behavioural semantics of group-based applications using the intermediate format FIACRE. We have experimented with model-checking of such systems, using the CADP verification toolset, and in particular the distributor tool. This allowed us to generate very large but finite state-space on the PacaGrid cloud infrastructure. We have then been able to compare different techniques for generating state-spaces, and experiment with different sizes of the modelled system and of the experimental platform.
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Eric Madelaine Connect in order to contact the contributor
Submitted on : Tuesday, November 23, 2010 - 10:26:09 AM
Last modification on : Thursday, August 4, 2022 - 4:52:45 PM
Long-term archiving on: : Thursday, February 24, 2011 - 2:27:22 AM


Files produced by the author(s)


  • HAL Id : inria-00538499, version 1



Ludovic Henrio, Eric Madelaine. Experiments with distributed Model-Checking of group-based applications. Sophia-Antipolis Formal Analysis Workshop, Oct 2010, Sophia-Antipolis, France. 3p. ⟨inria-00538499⟩



Record views


Files downloads