GRL2LNT Translator from GALS Representation Language to LNT

Organisation:	CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
Functionality:	Translation from GRL (GALS Representation Language) to LNT.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2013-2016
Description:	A GALS (Globally Asynchronous, Locally Synchronous) system consists of several components that evolve concurrently and interact with each other asynchronously. The design of GALS systems is tedious and error-prone due to the high degree of synchronous and asynchronous concurrency present in complex architectures. GRL is a formal language designed to model GALS systems, for the purpose of formal verification of the asynchronous aspects. GRL combines the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. It makes possible a modular description of synchronous components, environment constraints, and asynchronous communications. This verification can be done using CADP via a translation from GRL to the LNT input language of CADP. The translation is implemented in a software tool named GRL2LNT.
Conclusions:	TheGRL2LNT approach makes possible the analysis of GRL descriptions using the rich functionalities of CADP (e.g., simulation, verification, performance evaluation), with a focus on the asynchronous behaviour of GALS systems. In particular, hardware/software co-simulation is possible by using the EXEC/CAESAR framework of CADP, which enables the C code generated from a GRL description to be integrated with a physical platform.
Publications:	[Jebali-Lang-Mateescu-14-a] Fatma Jebali, Frederic Lang, and Radu Mateescu. "GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems (Syntax and Formal Semantics)". INRIA Research Report RR-8527, April 2014. Available on-line at: https://hal.inria.fr/hal-00983711v3 or from the CADP Web site in PDF or PostScript [Jebali-Lang-Mateescu-14-b] Fatma Jebali, Frederic Lang, and Radu Mateescu. "GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems". Proceedings of the 16th International Conference on Formal Engineering Methods ICFEM'2014, Lecture Notes in Computer Science vol. 8829, pp. 219-324, November 2014. Available on-line at: https://hal.inria.fr/hal-01082348 or from the CADP Web site in PDF or PostScript [Jebali-Lang-Mateescu-16] Fatma Jebali, Frederic Lang, and Radu Mateescu. "Formal Modelling and Verification of GALS Systems using GRL and CADP". In Formal Aspects of Computing, Springer, June 2016. Available on-line at: https://hal.inria.fr/hal-01290449 or from the CADP Web site in PDF or PostScript
Contact:	Fatma Jebali Inria Grenoble Rhône Alpes CONVECS team 655, avenue de l'Europe 38330 Montbonnot FRANCE Tel: +33 (0)4 76 61 54 15 Email: Fatma.Jebali@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