Translation Validation of (Multi-Clocked) SIGNAL Specifications

Organisation:	INRIA Centre Rennes-Bretagne Atlantique, IRISA/CNRS (FRANCE)
Method:	FIACRE
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems.
Period:	2010
Size:	n/a
Description:	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 generated automatically. 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.
Conclusions:	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.
Publications:	[Peralta-Gautier-Besnard-Guernic-10] 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, pages 199-208. Available on-line at: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5558632&tag=1 or from the CADP Web site: PDF PostScript
Contact:	Julio C. Peralta INRIA Centre Rennes-Bretagne Atlantique IRISA/CNRS Campus Universitaire de Beaulieu 35042 Rennes cedex FRANCE Email: Julio.Peralta@irisa.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page