Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

TL;DR

This paper introduces the first mechanically verified translation algorithm for hierarchical block diagrams, ensuring semantic equivalence across different translation strategies using formal proof in Isabelle.

Contribution

It presents a nondeterministic translation algorithm for HBDs with proven semantic determinacy, formalized and verified in Isabelle theorem prover.

Findings

The translation algorithm is semantically deterministic for all inputs.

Different translation strategies produce semantically equivalent results.

All proofs are formalized in the Isabelle theorem prover.

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.