INRIA Centre Rennes-Bretagne Atlantique, IRISA/CNRS (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
Critical embedded systems require guarantees on the reliability of
their implementation. Such a guarantee either takes the form of a
certified compiler, or the validation of each translation from
specification to implementation. This work considers the latter
approach, by translating both the SIGNAL specification of an embedded
system and the associated C simulator into Labelled Transition Systems
(LTSs). Then, an appropriate (successful) preorder test between both
LTSs can be interpreted as a refinement between the C implementation
and its source SIGNAL specification; otherwise, counter-examples are
Starting from a multi-clocked SIGNAL specification, a C implementation is automatically generated. From this C implementation, a description in FIACRE is extracted automatically and fed to CADP in order to generate the corresponding LTS. In parallel, another LTS is generated directly from the SIGNAL specification. An analysis of the equivalence and preorder of the two LTSs using the BISIMULATOR tool of CADP indicates whether the C program is an accurate implementation of the SIGNAL specification. The approach is illustrated on two FIFO queues with one and two places, respectively.
For a critical system, it is vital that both the specification and its
implementation are reliable. Model checking of a specification is not
unusual, but this case study demonstrates the application of model
checking for comparing a specification with its implementation.
At high-level, the approach is simple and elegant, and the automated
translators and algorithms available means it can be applied in
practice, demonstrating the value of using CADP to validate
implementations that are based on SIGNAL specifications.
Julio C. Peralta, Thierry Gautier, Loic Besnard, and Paul Le Guernic.
"LTSs for Translation Validation of (multi-clocked) SIGNAL
specifications". Proceedings of the 8th IEEE/ACM International
Conference on Formal Methods and Models for Codesign MEMOCODE'10,
Available on-line at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5558632&tag=1
or from our FTP site: PDF PostScript
Julio C. Peralta
INRIA Centre Rennes-Bretagne Atlantique
Campus Universitaire de Beaulieu
35042 Rennes cedex
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|