טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentRyabtsev Michael
SubjectTranslation Validation: from Simulink to C
DepartmentDepartment of Computer Science
Supervisor Professor Ofer Strichman
Full Thesis textFull thesis text - English Version


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.