Debugging and Verification Tools for LINGUA FRANCA in GEMOC Studio

Organisation:	INRIA Sophia Antipolis - Méditerranée and I3S laboratory (FRANCE) NOVA University Lisbon (PORTUGAL) University of Texas at Dallas and University of California at Berkeley (USA)
Functionality:	Debugging
Tools used:	GEMOC Studio CADP (Construction and Analysis of Distributed Processes)
Period:	2021
Description:	Cyber-physical systems (CPSs) are becoming increasingly complex, containing an intricate composition of complicated software, hardware, and networked systems, which makes their development difficult and error-prone. The management of concurrency, timing, and distributed computing are therefore increasingly challenging. A comprehensive solution is proposed in the form of LINGUA FRANCA (LF), a polyglot coordination language for the deterministic composition of concurrent, time-sensitive, and potentially distributed reactive components (called reactors). LF is aimed at simplifying the design and implementation of CPSs through a programming model with sophisticated runtime support that delivers deterministic behavior under quantifiable assumptions. The extension of LF with support for more target languages raises the issues of debugging the underlying code generators and runtime libraries, as well as debugging an LF program itself. This work proposes an advanced debugging framework for LF, built using GEMOC Studio, encompassing two methods. The first method is interactive debugging, which involves the weaving of an abstract execution model of LF into its syntactic definition, such that LF reaction code can be interpreted through this abstract model. This enables to implement a rich debugging environment, equipped with forward and backward timed exploration, inspection of LF program states, graphical animation, and exhaustive simulation of the program. This last functionality makes possible to verify an LF program by feeding the underlying state space and the desired MCL temporal formulas to the EVALUATOR model checker of CADP. The diagnostics produced by the model checker can be injected into the debugging environment. The second method is trace debugging, which involves the injection of execution traces obtained by executing compiled LF programs directly in the development environment. This enables target runtime developers to validate execution traces obtained through a standardized tracing interface against the LF semantics, and detect any deviation thereof from the correct behavior.
Conclusions:	This work proposes a framework for analyzing and debugging LF programs and runtime implementations. The framework was built using the GEMOC approach, in which the language artifacts are augmented in the existing compiler implementation with instrumentation encoding the operational semantics of the language. This approach provides access to advanced functionalities, such as omniscient debugging, exhaustive simulation and model checking, and diagram animation.
Publications:	[Deantoni-Cambeiro-Bateni-et-al-21] "Debugging and Verification Tools for LINGUA FRANCA in GEMOC Studio". Proc. of the 24th Forum on specification & Design Languages (FDL'2021), Antibes, France, pp. 1-8. IEEE, Sep. 2021. Available on-line at: https://hal.uca.fr/I3S/hal-03374955 or from the CADP Web site in PDF or PostScript
Contact:	Julien Deantoni Laboratoire I3S - UNS / CNRS UMR 7271 INRIA Sophia Antipolis Méditerranée 2004, route des Lucioles (Lagrange L-0041) BP93 F-06902 Sophia Antipolis FRANCE Email: julien.deantoni@univ-cotedazur.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