Sciweavers

MEMOCODE
2010
IEEE

LTSs for translation validation of (multi-clocked) SIGNAL specifications

13 years 1 months ago
LTSs for translation validation of (multi-clocked) SIGNAL specifications
Design of critical embedded systems demands for guarantees on the reliability of the implementation/compilation of a specification. In general, this guarantee takes either the form of a certified compiler, or the validation of each translation. Here we adopt the translation validation approach. In particular, we translate both the SIGNAL specification and the associated C simulator into 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. The feasibility of our approach is shown through examples. Keywords-Labelled Transition Systems; Multi-clocked Synchronous Programs; Concurrent Programs; Refinement
Julio C. Peralta, Thierry Gautier, Loïc Besna
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where MEMOCODE
Authors Julio C. Peralta, Thierry Gautier, Loïc Besnard, Paul Le Guernic
Comments (0)