Translating Hierarchical Block Diagrams into Composite Predicate Transformers
Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis

TL;DR
This paper presents methods for translating hierarchical block diagrams from Simulink into a formal algebra of predicate transformers, enabling formal verification of embedded control systems.
Contribution
It introduces three translation algorithms for converting Simulink models into a formal algebra, with a prototype tool and case studies demonstrating their effectiveness.
Findings
Different translation algorithms offer tradeoffs in size and readability.
The prototype tool successfully translates Simulink models into formal algebraic terms.
Case studies include a benchmark model by Toyota.
Abstract
Simulink is the de facto industrial standard for designing embedded control systems. When dealing with the formal verification of Simulink models, we face the problem of translating the graphical language of Simulink, namely, hierarchical block diagrams (HBDs), into a formalism suitable for verification. In this paper, we study the translation of HBDs into the compositional refinement calculus framework for reactive systems. Specifically, we consider as target language an algebra of atomic predicate transformers to capture basic Simulink blocks (both stateless and stateful), composed in series, in parallel, and in feedback. For a given HBD, there are many possible ways to translate it into a term in this algebra, with different tradeoffs. We explore these tradeoffs, and present three translation algorithms. We report on a prototype implementation of these algorithms in a tool that…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsEmbedded Systems Design Techniques · Parallel Computing and Optimization Techniques · VLSI and FPGA Design Techniques
