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.
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 ).
@cite_18 @cite_4 @cite_52 @cite_3 @cite_17
2115803389 1964587130 2039706992 2242425235
We present a method of translating discrete-time Simulink models to Lustre programs. Our method consists of three steps: type inference, clock inference, and hierarchical bottom-up translation. In the process, we explain and formalize the typing and timing mechanisms of Simulink. The method has been implemented in a prototype tool called S2L, which has been used in the context of a European research project to translate two automotive controller models provided by Audi. We present a method for the translation of a discrete-time fragment of Simulink into the synchronous subset of the BIP language. The translation is fully compositional, that is, it preserves completely the original structure and reveals the minimal control coordination structure needed to perform the correct computation within Simulink models. Additionally, this translation can be seen as providing an alternative operational semantics of Simulink models using BIP. The advantages are twofold. It allows for integration of Simulink models within heterogeneous BIP designs. It enables the use of validation and automatic implementation techniques already available for BIP on Simulink models. The translation is currently implemented in the Simulink2BIP tool. We report several experiments, in particular, we show that the executable code generated from BIP models has comparable runtime performances as the code produced by the Real-Time Workshop on several Simulink models. We develop a semantic translation approach for Simulink diagrams. Simulink is a graphical tool for representing and simulating dynamical systems. We propose a recursive approach for translating a class of Simulink diagrams to input output-extended finite automata (I O-EFA). An I O-EFA model of a Simulink diagram can be used for further analysis such as test generation and formal verification. We show that the translation approach is sound and complete: The input-state-output behavior of an I O-EFA model, as defined in terms of a step-trajectory, preserves the input-state-output behavior of the corresponding Simulink diagram at each sample time (assuming the same integration method for any of the continuous blocks with dynamics). This dissertation perceives a similarity between two activities: that of coordinating the search for simulation traces toward reaching verification closure, and that of coordinating the search for a proof within a theorem prover. The programmatic coordination of simulation is difficult with existing tools for digital circuit verification because stimuli generation, simulation execution, and analysis of simulation results are all decoupled. A new programming language to address this problem, analogous to the mechanism for orchestrating proof search tactics within a theorem prover, is defined wherein device simulation is made a first-class notion. This meta-language for functional verification is first formalized in a parametric way over hardware description languages using rewriting logic, and subsequently a more richly featured software tool for Verilog designs, implemented as an embedded domain-specific language in Haskell, is described and used to demonstrate the novelty of the programming language and to conduct two case studies. Additionally, three hardware description languages are given formal semantics using rewriting logic and we demonstrate the use of executable rewriting logic tools to formally analyze devices implemented in those languages.