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

Hugues Evrard

Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2016 (Eindhoven, The Netherlands), April 2-8, 2016

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.

6 pages

PDF

PostScript

Slides of H. Evrard's lecture at TACAS'2016:

PDF