Mechanically proving determinacy of hierarchical block diagram translations
Loading...
Access rights
openAccess
URL
Journal Title
Journal ISSN
Volume Title
A4 Artikkeli konferenssijulkaisussa
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
Other link related to publication (opens in new window)
Date
Department
Major/Subject
Mcode
Degree programme
Language
en
Pages
24
Series
Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings, pp. 577-600, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ; Volume 11388 LNCS
Abstract
Hierarchical block diagrams (HBDs) are at the heart of embedded system design tools, including Simulink. Numerous translations exist from HBDs into languages with formal semantics, amenable to formal verification. However, none of these translations has been proven correct, to our knowledge. We present in this paper the first mechanically proven HBD translation algorithm. The algorithm translates HBDs into an algebra of terms with three basic composition operations (serial, parallel, and feedback). In order to capture various translation strategies resulting in different terms achieving different tradeoffs, the algorithm is nondeterministic. Despite this, we prove its semantic determinacy: for every input HBD, all possible terms that can be generated by the algorithm are semantically equivalent. We apply this result to show how three Simulink translation strategies introduced previously can be formalized as determinizations of the algorithm, and derive that these strategies yield semantically equivalent results (a question left open in previous work). All results are formalized and proved in the Isabelle theorem-prover and the code is publicly available.Description
| openaire: EC/H2020/730080/EU//ESROCOS
Keywords
Other note
Citation
Preoteasa, V, Dragomir, I & Tripakis, S 2019, Mechanically proving determinacy of hierarchical block diagram translations. in R Piskac & C Enea (eds), Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11388 LNCS, Springer, pp. 577-600, International Conference on Verification, Model Checking, and Abstract Interpretation, Cascais, Portugal, 13/01/2019. https://doi.org/10.1007/978-3-030-11245-5_27