Partial translation verification for untrusted code-generators

Matthew Staats; Mats Heimdahl

doi:10.1007/978-3-540-88194-0_15

Partial translation verification for untrusted code-generators

Matthew Staats, Mats Heimdahl

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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	https://doi.org/10.1007/978-3-540-88194-0_15
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.

Access

10.1007/978-3-540-88194-0_15

OpenUrl availability

Full text

Cite this

Staats, M., & Heimdahl, M. (2008). Partial translation verification for untrusted code-generators. In Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings (pp. 226-237). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5256 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-88194-0_15

Partial translation verification for untrusted code-generators. / Staats, Matthew; Heimdahl, Mats.
Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings. Springer Verlag, 2008. p. 226-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5256 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Staats, M & Heimdahl, M 2008, Partial translation verification for untrusted code-generators. in Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5256 LNCS, Springer Verlag, pp. 226-237, 10th International Conference on Formal Engineering Methods, ICFEM 2008, Kitayushu-City, Japan, 10/27/08. https://doi.org/10.1007/978-3-540-88194-0_15

Staats M, Heimdahl M. Partial translation verification for untrusted code-generators. In Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings. Springer Verlag. 2008. p. 226-237. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-88194-0_15

Staats, Matthew ; Heimdahl, Mats. / Partial translation verification for untrusted code-generators. Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings. Springer Verlag, 2008. pp. 226-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a9a51a03aabb4aea98cc6441e851630a,

title = "Partial translation verification for untrusted code-generators",

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.",

author = "Matthew Staats and Mats Heimdahl",

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.; 10th International Conference on Formal Engineering Methods, ICFEM 2008 ; Conference date: 27-10-2008 Through 31-10-2008",

year = "2008",

doi = "10.1007/978-3-540-88194-0_15",

language = "English (US)",

isbn = "354088193X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "226--237",

booktitle = "Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings",

}

TY - GEN

T1 - Partial translation verification for untrusted code-generators

AU - Staats, Matthew

AU - Heimdahl, Mats

N1 - 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.

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=57049178478&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57049178478&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-88194-0_15

DO - 10.1007/978-3-540-88194-0_15

M3 - Conference contribution

AN - SCOPUS:57049178478

SN - 354088193X

SN - 9783540881933

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 226

EP - 237

BT - Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings

PB - Springer Verlag

T2 - 10th International Conference on Formal Engineering Methods, ICFEM 2008

Y2 - 27 October 2008 through 31 October 2008

ER -

Partial translation verification for untrusted code-generators

Abstract

Publication series

Other

Bibliographical note

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this