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 2085838366 2172166122 1982828147 2091676842 2296004247 1627668763
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. Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves the?-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch. Many researchers have explored the relation between discrete-time recurrent neural networks (DTRNN) and finite-state machines (FSMs) either by showing their computational equivalence or by training them to perform as finite-state recognizers from examples. Most of this work has focused on the simplest class of deterministic state machines, that is deterministic finite automata and Mealy (or Moore) machines. The class of translations these machines can perform is very limited, mainly because these machines output symbols at the same rate as they input symbols, and therefore, the input and the translation have the same length; one may call these translations synchronous. Real-life translations are more complex: word reorderings, deletions, and insertions are common in natural-language translations; or, in speech-to-phoneme conversion, the number of frames corresponding to each phoneme is different and depends on the particular speaker or word. There are, however, simple deterministic, finite-state machines (extensions of Mealy machines) that may perform these classes of "asynchronous" or "time-warped" translations. A simple DTRNN model with input and output control lines inspired on this class of machines is presented and successfully applied to simple asynchronous translation tasks with interesting results regarding generalization. Training of these nets from input-output pairs is complicated by the fact that the time alignment between the target output sequence and the input sequence is unknown and has to be learned: we propose a new error function to tackle this problem. This approach to the induction of asynchronous translators is discussed in connection with other approaches. Simulink is an industrial de-facto standard for building executable models of embedded systems and their environments, facilitating validation by simulation. Due to the inherent incompleteness of this form of system validation, complementing simulation by formal verification would be desirable. A prerequisite for such an approach is a formal semantics of Simulink's graphical models. In this paper, we show how to encode Simulink diagrams into Hybrid CSP (HCSP), a formal modelling language encoding hybrid system dynamics by means of an extension of CSP. The translation from Simulink to HCSP is fully automatic. We furthermore discuss how to utilize a Hybrid Hoare Logic Prover to verify the translated HCSP models. We demonstrate our approach on a combined scenario originating from the Chinese High-speed Train Control System at Level 3 (CTCS-3). Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of π-Calculus processes into place transition Petri nets. Our translation exploits the connections created by restricted names and can yield finite nets even for processes with unbounded name and unbounded process creation. The property of structural stationarity characterises the processes mapped to finite nets. We provide exact conditions for structural stationarity using novel characteristic functions. As application of the theory, we identify a rich syntactic class of structurally stationary processes, called finite handler processes. Our Petri net translation facilitates the automatic verification of a case study modelled in this class. Simulink is an industrial de-facto standard for building executable models of control systems and their environments. Stateflow is a toolbox used to model reactive systems via hierarchical statecharts within a Simulink model, extending Simulink’s scope to event-driven and hybrid forms of embedded control. In safety-critical control systems, exhaustive coverage of system dynamics by formal verification would be desirable, being based on a formal semantics of combined Simulink Stateflow graphical models. In our previous work, we addressed the problem of formal verification of pure Simulink diagrams via an encoding into HCSP, a formal modelling language encoding hybrid system dynamics by means of an extension of CSP. In this paper, we extend the approach to cover Simulink models containing Stateflow components also. The transformation from Simulink Stateflow to HCSP is fully automatic, and the formal verification of the encoding is supported by a Hybrid Hoare Logic (HHL) prover based on Isabelle HOL. We demonstrate our approach by a real world case study originating from the Chinese High-speed Train Control System (CTCS-3). In this paper, we address the problem of local search for the falsification of hybrid automata with affine dynamics. Namely, if we are given a sequence of locations and a maximum simulation time, we return the trajectory that comes the closest to the unsafe set. In order to solve this problem, we formulate it as a differentiable optimization problem which we solve using Sequential Quadratic Programming. The purpose of developing such a local search method is to combine it with high level stochastic optimization algorithms in order to falsify hybrid systems with complex discrete dynamics and high dimensional continuous spaces. Experimental results indicate that indeed the local search procedure improves upon the results of pure stochastic optimization algorithms.