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.
Several translations from Simulink have been proposed in the literature, including to Hybrid Automata @cite_0 , BIP @cite_23 , NuSMV @cite_42 , Lustre @cite_2 , Boogie @cite_33 , Timed Interval Calculus @cite_10 , Function Blocks @cite_3 , I O Extended Finite Automata @cite_12 , Hybrid CSP @cite_46 , and SpaceEx @cite_48 . It is unclear to what extent these approaches provide formal guarantees on the determinism of the translation. For example, the order in which blocks in the Simulink diagram are processed might a-priori influence the result. Some works fix this order, e.g., @cite_33 computes the control flow graph and translates the model according to this computed order. In contrast, we prove that the results of our algorithm are equivalent for any order. To the best of our knowledge, the abstract translation proposed hereafter for Simulink is the only one formally defined and mechanically proven correct.
@cite_33 @cite_48 @cite_42 @cite_3 @cite_0 @cite_23 @cite_2 @cite_46 @cite_10 @cite_12
2115803389 1964587130 2039706992 2024215898
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). We study efficient translations of Regular Linear Temporal Logic ( ) into automata on infinite words. is a temporal logic that fuses Linear Temporal Logic (LTL) with regular expressions, extending its expressive power to all @math -regular languages. The first contribution of this paper is a novel bottom up translation from into alternating parity automata of linear size that requires only colors @math , @math and @math . Moreover, the resulting automata enjoy the stratified internal structure of hesitant automata. Our translation is defined inductively for every operator, and does not require an upfront transformation of the expression into a normal form. Our construction builds at every step two automata: one equivalent to the formula and another to its complement. Inspired by this construction, our second contribution is to extend with new operators, including universal sequential composition, that enrich the logic with duality laws and negation normal forms. The third contribution is a ranking translation of the resulting alternating automata into non-deterministic automata. To provide this efficient translation we introduce the notion of stratified rankings, and show how the translation is optimal for the LTL fragment of the logic.