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.
@cite_18: The industrial tool Matlab Simulink is widely used in the design of embedded systems. The main feature of this tool is its ability to model in a common formalism the software and its physical environment. This makes it very useful for validating the design of embedded software using numerical simulation. However, the formal verification of such models is still problematic as Simulink is a programming language for which no formal semantics exists. In this article, we present an operational semantics of a representative subset of Simulink which includes both continuous-time and discrete-time blocks. We believe that this work gives a better understanding of Simulink and it defines the foundations of a general framework to apply formal methods on Simulink's high level descriptions of embedded systems.
@cite_4: We present a compositional semantics and analysis framework for hierarchical block diagrams (HBDs) in terms of atomic and composite predicate transformers. Our framework consists of two components: (1) a compiler that translates Simulink HBDs into an algebra of transformers composed in series, in parallel, and in feedback; (2) an implementation of the theory of transformers and static analysis techniques for them in Isabelle. We evaluate our framework on several case studies including a benchmark Simulink model by Toyota.
@cite_52: 
@cite_3: Abstract In this paper, a new model-based engineering approach is introduced by bridging MATLAB Simulink with IEC61499 Function Block models. This is achieved by a transformation between the two block-diagram languages. The transformation supported by the developed tools sets the cornerstone of the verification and validation framework for IEC 61499 Function Blocks in closed-loop with the models of the plant. The framework also paves the way to running distributed simulations of complex hybrid (i.e., continuous-discrete) closed-loop plant-controller systems and building complex models using the efficient object instantiation techniques of IEC 61499.
@cite_17: Translation validation is a technique for formally establishing the semantic equivalence of the source and the target of a code generator. In this work we present a translation validation tool for the Real-Time Workshop code generator that receives as input Simulink models and generates optimized C code.
The focus of several works is to validate the preservation of the semantics of the original diagram by the resulting translation (e.g., see @cite_3 @cite_17 @cite_18 @cite_52 ). In contrast, our goal is to prove equivalence of all possible translations. Given that Simulink semantics is informal ( what the simulator does''), ultimately the only way to gain confidence that the translation conforms to the original Simulink model is by simulation (e.g., as in @cite_4 ).