LTSs for Translation Validation of (multi-clocked) Signal specifications

International audienceDesign 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