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)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
"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
Laboratoire I3S - UNS / CNRS UMR 7271
INRIA Sophia Antipolis Méditerranée
2004, route des Lucioles (Lagrange L-0041)
F-06902 Sophia Antipolis
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|