Model-checking Distributed Applications with GRAS

Cristian Rosa (1) , Martin Quinson (1) , Stephan Merz (2)

1 ALGORILLE - Algorithms for the Grid
2 MOSEL - Proof-oriented development of computer-based systems

In this paper, we present our work to add a model-checker to the GRAS framework. This tool provides a development environment allowing debug real applications within the simulator before deploying them on real platforms. We discuss the main difficulties to integrate such a model-checker, and present our approach to solve them, as well as a prototype implementation.

Mots clés: model-checking; distributed systems; simulation

Domaines: Modélisation et simulation

Cristian Rosa, Martin Quinson, Stephan Merz. Model-checking Distributed Applications with GRAS. [Research Report] RR-7052, INRIA. 2009, pp.11. ⟨inria-00422159⟩