Translating Hierarchical Block Diagrams into Composite Predicate Transformers

Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis

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 translatin…