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 language | English (US) |
---|---|
Title of host publication | Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings |
Publisher | Springer Verlag |
Pages | 226-237 |
Number of pages | 12 |
ISBN (Print) | 354088193X, 9783540881933 |
DOIs | |
State | Published - 2008 |
Event | 10th International Conference on Formal Engineering Methods, ICFEM 2008 - Kitayushu-City, Japan Duration: Oct 27 2008 → Oct 31 2008 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 5256 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Other
Other | 10th International Conference on Formal Engineering Methods, ICFEM 2008 |
---|---|
Country/Territory | Japan |
City | Kitayushu-City |
Period | 10/27/08 → 10/31/08 |
Bibliographical note
Funding Information:This work has been partially supported by NASA Ames Research Center Cooperative Agreement NNA06CB21A, NASA IV&V Facility Contract NNG-05CB16C, and the L-3 Titan Group.