Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 11:00 - 11:30 at Sala III - Software Verification and Synthesis Chair(s): Ori Lahav

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 {\em 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.

Presentation (presentation.pdf)480KiB

Tue 15 Jan
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

11:00 - 12:30: VMCAI 2019 - Software Verification and Synthesis at Sala III
Chair(s): Ori LahavTel Aviv University
VMCAI-201911:00 - 11:30
Viorel Preoteasa, Iulia Dragomir, Stavros TripakisAalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
VMCAI-201911:30 - 12:00
VMCAI-201912:00 - 12:30
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison