Partial translation verification for untrusted code-generators

Matthew Staats, Mats Heimdahl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings
Pages226-237
Number of pages12
DOIs
StatePublished - Dec 8 2008
Event10th International Conference on Formal Engineering Methods, ICFEM 2008 - Kitayushu-City, Japan
Duration: Oct 27 2008Oct 31 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5256 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other10th International Conference on Formal Engineering Methods, ICFEM 2008
CountryJapan
CityKitayushu-City
Period10/27/0810/31/08

Fingerprint Dive into the research topics of 'Partial translation verification for untrusted code-generators'. Together they form a unique fingerprint.

Cite this