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.
Document type :
Conference papers
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

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01087505
Contributor : Gwen Salaün <>
Submitted on : Tuesday, January 20, 2015 - 10:34:21 AM
Last modification on : Wednesday, December 14, 2016 - 1:08:45 AM
Document(s) archivé(s) le : Tuesday, April 21, 2015 - 10:23:05 AM

File

main-VMCAI.pdf
Files produced by the author(s)

Identifiers

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〉

Share

Metrics

Record views

311

Document downloads

89