DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation

Hugues Evrard 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Formal methods can verify the correctness of a concurrent system by analyzing its model. However, if the actual implementation is written by hand, subtle and hard to detect bugs may be unintentionally introduced, thus ruining the verification effort. In this paper, we present DLC (Distributed LNT Compiler), a tool that automatically generates distributed implementation of concurrent systems modeled in the LNT language, which can be formally verified using the CADP toolbox.
Document type :
Conference papers
TACAS'2016, Apr 2016, Eindhoven, Netherlands. Springer-Verlag, 2016, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2016. <10.1007/978-3-662-49674-9_34>
Liste complète des métadonnées


https://hal.inria.fr/hal-01250925
Contributor : Frederic Lang <>
Submitted on : Tuesday, March 29, 2016 - 11:10:58 AM
Last modification on : Thursday, May 12, 2016 - 9:43:11 AM
Document(s) archivé(s) le : Thursday, June 30, 2016 - 12:06:41 PM

File

Evrard_TACAS_2016.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Hugues Evrard. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation. TACAS'2016, Apr 2016, Eindhoven, Netherlands. Springer-Verlag, 2016, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2016. <10.1007/978-3-662-49674-9_34>. <hal-01250925>

Share

Metrics

Record views

214

Document downloads

51