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

• Type: Journal
• Year: 2010
• Where: MEMOCODE
• Authors: Julio C. Peralta, Thierry Gautier, Loïc Besnard, Paul Le Guernic
• Keywords: Critical Embedded Systems, Formal Methods, MEMOCODE 2010, SIGNAL Specification, Translation Validation Approach