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 protocol (see http://cadp.inria.fr/case-studies/15-g-raft.html ): 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 Frédéric 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 the CADP Web 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 the CADP Web site in PDF or PostScript [Evrard-Lang-17] Hugues Evrard and Frédéric Lang. "Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous". Journal of Logical and Algebraic Methods in Programming 88:121-153, 2017. Available on-line at: http://cadp.inria.fr/publications/Evrard-Lang-17.html or from the CADP Web 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

Back to the CADP research tools page