Debugging Process Algebra Specifications

Gwen Salaün 1 Lina Ye 2
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Designing and developing distributed and concurrent applications has always been a tedious and error-prone task. In this context, formal techniques and tools are of great help in order to specify such concurrent systems and detect bugs in the corresponding models. In this paper, we propose a new framework for debugging value-passing process algebra through coverage analysis. We illustrate our approach with LNT, which is a recent specification language designed for formally modelling concurrent systems. We define several coverage notions before showing how to instrument the specification without affecting original behaviors. Our approach helps one to improve the quality of a dataset of examples used for validation purposes, but also to find ill-formed decisions, dead code, and other errors in the specification. We have implemented a tool for automating our debugging approach, and applied it to several real-world case studies in different application areas.
Type de document :
Communication dans un congrès
VMCAI 2015, Jan 2015, Mumbai, India. Springer, 8931, pp.18, 〈10.1007/978-3-662-46081-8_14〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
Contributeur : Gwen Salaün <>
Soumis le : mardi 20 janvier 2015 - 10:34:21
Dernière modification le : samedi 15 décembre 2018 - 01:49:55
Document(s) archivé(s) le : mardi 21 avril 2015 - 10:23:05


Fichiers produits par l'(les) auteur(s)



Gwen Salaün, Lina Ye. Debugging Process Algebra Specifications. VMCAI 2015, Jan 2015, Mumbai, India. Springer, 8931, pp.18, 〈10.1007/978-3-662-46081-8_14〉. 〈hal-01087505v2〉



Consultations de la notice


Téléchargements de fichiers