University of Minnesota
Software Engineering Center

You are here

Partial Translation Verification for Untrusted Code-Generators

Date of Publication: 
October 2008
Associated Research Groups: 
Publication Files: 
Within the context of model-based development, the correctness of code generators for modeling notations such as Simulink and Stateflow is of obvious importance. If correctness of code generation can be shown, the extensive and often costly verification and validation activities conducted in the modeling domain could be effectively leveraged in the code domain. Unfortunately, most code generators in use today give no guarantees of correctness. In this paper, we investigate a method of leveraging existing model checking tools to verify the partial correctness of code generated by code generators that offer no guarantees of correctness. We explore the feasibility of this approach through a prototype tool that allows us to verify that Linear Temporal Logic (LTL) safety properties are preserved by C code generators for Simulink models. We find that the approach scales well, allowing us to verify that 55 LTL properties are maintained when generating 12,000+ lines of C code from a large Simulink model.
10th International Conference on Formal Methods and Software Engineering (ICFEM '08)
@inproceedings{Staats:2008:PTV:1482985.1483006, author = {Staats, Matthew and Heimdahl, Mats P.}, title = {Partial Translation Verification for Untrusted Code-Generators}, booktitle = {Proceedings of the 10th International Conference on Formal Methods and Software Engineering}, series = {ICFEM '08}, year = {2008}, isbn = {978-3-540-88193-3}, location = {Kitakyushu-City, Japan}, pages = {226--237}, numpages = {12}, url = {}, doi = {}, acmid = {1483006}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, }