Skip to Main content Skip to Navigation
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 metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/inria-00538499
Contributor : Eric Madelaine <>
Submitted on : Tuesday, November 23, 2010 - 10:26:09 AM
Last modification on : Tuesday, May 26, 2020 - 6:50:22 PM
Long-term archiving on: : Thursday, February 24, 2011 - 2:27:22 AM

File

05_Madelaine_SAFA2010_final.pd...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00538499, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

362

Files downloads

151