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

https://hal.inria.fr/hal-01087505
Contributeur : Gwen Salaün <>
Soumis le : mardi 20 janvier 2015 - 10:34:21
Dernière modification le : mercredi 14 décembre 2016 - 01:08:45
Document(s) archivé(s) le : mardi 21 avril 2015 - 10:23:05

Fichier

main-VMCAI.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de
la notice

311

Téléchargements du document

89