Technical Report MSC-2009-13

TR#:MSC-2009-13
Class:MSC
Title: Translation validation: from Simulink to C
Authors: Michael Ryabtsev
Supervisors: Ofer Strichman
PDFMSC-2009-13.pdf
Abstract: Translation validation is a technique for formally establishing the semantic equivalence of a source and a target of a code generator. A translation validation tool receives as input the source and target programs as well as a mapping between their input, output and state variables. Based on the semantics of the source and target languages, it then builds a verification condition that is valid if and only if the generated code faithfully preserves the semantics of the source code. Hence, translation validation is applied separately to each translation, in contrast to the alternative of verifying the code generator itself. It has the advantage of being less sensitive to changes in the code generator (such changes invalidate correctness proofs of the code generator) and simpler, since verifying the code generator amounts of functional verification of a complex program. Simulink, developed by The MathWorks, is a software package for model-based design of dynamic systems such as signal processing, control and communications applications. The model-based design and development through the Simulink graphical language is argued to be faster and more cost effective than implementing the same system directly with some imperative or functional programming language. In addition Simulink models can be translated into an optimized C or C++ source code via the Real-Time Workshop code generator.

In this work we present TVS (Translation Validation tool for Simulink) which addresses the problem of proving the semantic equivalence between a Simulink model and a C program that was generated by Real-Time Workshop from that model. TVS receives as an input the Simulink model and the generated C program, automatically finds a mapping between their variables, and generates a verification condition, which is valid only if the translation is correct. The verification condition can be checked automatically with an automatic theorem-proving tool, or, as in our case, with an SMT solver called Yices.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2009/MSC/MSC-2009-13), rather than to the URL of the PDF or PS files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2009
To the main CS technical reports page

Computer science department, Technion