Database of Research Tools Developed Using CADP

DLC Compiler from LNT to Distributed C Code

Organisation: CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)

Functionality: Compilation from LNT formal models to Distributed C Code

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2012-2016

Description: When designing concurrent systems, the use of formal methods often consists in verifying not the system implementation itself, but a model of the system. The actual system implementation is generally written by hand, after the verification phase. Writing a correct implementation can be tedious and error-prone, especially in the context of distributed systems, which are notoriously complex. The automatic generation of distributed implementations directly from formal models is preferrable as it can speed up the production of software, while letting the programmer operate at the formal model level, with the benefits of formal verification tools.
In the framework of CADP, the tool DLC (Distributed LNT Compiler) enables distributed implementations of concurrent systems to be generated automatically from their LNT formal model. DLC produces several executables, which can be deployed on distinct computers. Moreover, DLC lets the end user optionally define interactions between the implementation and its physical environment. DLC does not require any special annotations in the LNT source and process interactions by multiway rendezvous with data exchange are managed by a formally verified protocol.

Conclusions: Several distributed implementations have been generated automatically from their formal LNT model using DLC. The biggest case-study so far is the Raft consensus algorithm: From an LNT model of about 500 lines, DLC produces more than 9000 lines of C code for a Raft server. Across all examples, results illustrate that implementations generated by DLC can achieve more than 1000 rendezvous in sequence per second, and of course much more when rendezvous are realized concurrently on different gates. This qualifies DLC at least for rapid prototyping.

Publications: [Evrard-Lang-15] Hugues Evrard and Frederic Lang. "Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes". Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing, Special Session on Formal Approaches to Parallel and Distributed Systems PDP/4PAD'2015, IEEE, March 2015.
Available on-line at: http://cadp.inria.fr/publications/Evrard-Lang-15.html
or from our FTP site in PDF or PostScript

[Evrard-16] Hugues Evrard. "DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation". Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2016, Lecture Notes in Computer Science vol. 9636, pp. 553-559, Springer, April 2016.
Available on-line at: http://cadp.inria.fr/publications/Evrard-16.html
or from our FTP site in PDF or PostScript

Contact:
Dr. Hugues Evrard
Inria Grenoble Rhône Alpes
CONVECS team
655, avenue de l'Europe
38330 Montbonnot
FRANCE
Tel: +33 (0)4 76 61 52 72
Email: Hugues.Evrard@inria.fr



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Tue Jun 21 17:03:03 2016.


Back to the CADP research tools page