Skip to Main content Skip to Navigation
New interface
Conference papers

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
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Gwen Salaün Connect in order to contact the contributor
Submitted on : Tuesday, January 20, 2015 - 10:34:21 AM
Last modification on : Wednesday, July 6, 2022 - 4:21:47 AM
Long-term archiving on: : Tuesday, April 21, 2015 - 10:23:05 AM


Files produced by the author(s)



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



Record views


Files downloads