SimGrid MC: Verification Support for a Multi-API Simulation Platform

Stephan Merz 1, 2 Martin Quinson 3 Cristian Rosa 3
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 ALGORILLE - Algorithms for the Grid
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : SimGrid MC is a stateless model checker for distributed systems that is part of the SimGrid Simulation Framework. It verifies implementations of distributed algorithms, written in C and using any of several communication APIs provided by the simulator. Because the model checker is fully integrated in the simulator that programmers use to validate their implementations, they gain powerful verification capabilities without having to adapt their code. We describe the architecture of SimGrid MC, and show how it copes with the state space explosion problem. In particular, we argue that a generic Dynamic Partial Order Reductions algorithm is effective for handling the different communication APIs that are provided by SimGrid. As a case study, we verify an implementation of Chord, where SimGrid MC helped us discover an intricate bug in a matter of seconds.
Type de document :
Communication dans un congrès
Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.274-288, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_18〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00593505
Contributeur : Stephan Merz <>
Soumis le : lundi 16 mai 2011 - 12:33:57
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Fichier

978-3-642-21461-5_18_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Stephan Merz, Martin Quinson, Cristian Rosa. SimGrid MC: Verification Support for a Multi-API Simulation Platform. Roberto Bruni; Juergen Dingel. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. Springer, Lecture Notes in Computer Science, LNCS-6722, pp.274-288, 2011, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-21461-5_18〉. 〈inria-00593505〉

Partager

Métriques

Consultations de la notice

240

Téléchargements de fichiers

45