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.