Mechanically proving determinacy of hierarchical block diagram translations

Viorel Preoteasa*, Iulia Dragomir, Stavros Tripakis

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

2 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
EditorsRuzica Piskac, Constantin Enea
Pages577-600
Number of pages24
DOIs
Publication statusPublished - 1 Jan 2019
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Verification, Model Checking, and Abstract Interpretation - Cascais, Portugal
Duration: 13 Jan 201915 Jan 2019
Conference number: 20

Publication series

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

Conference

ConferenceInternational Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated titleVMCAI
CountryPortugal
CityCascais
Period13/01/201915/01/2019

Fingerprint Dive into the research topics of 'Mechanically proving determinacy of hierarchical block diagram translations'. Together they form a unique fingerprint.

Cite this