| TR#: | MSC-2009-13 |
| Class: | MSC |
| Title: | Translation validation: from Simulink to C |
| Authors: | Michael Ryabtsev |
| Supervisors: | Ofer Strichman |
| MSC-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. |
| Copyright | The 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