Semantic Translation of Simulink Diagrams to Input/Output Extended Finite Automata

Abstract

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).

1 Introduction

Simulink/Stateflow (S/S) (Simulink 2010) diagrams are graphical representations of dynamical systems, and can capture both time-driven as well as event-driven dynamics of hybrid systems. Stateflow diagrams are used for representing and simulating event-driven dynamics. The S/S diagrams can be simulated to generate sample-runs (runs on sample times) which provide a means for their validation. Other means of validation include testing and verification. In order to be able to test a S/S diagram or verify an implementation of a S/S diagram, a model-based approach is desirable, where the model can be used for automated test generation or as a formal specification.

Simulink blocks can be time-driven or non time-driven. A time-driven block, such as an Integrator block, represents the time-dependent mathematical relationships between its inputs and outputs. On the other hand, non time-driven block, such as a Stateflow block or a Discrete Event Subsystem block, may evolve upon the occurrence of events. In this paper, we only study the semantic translation of time-driven blocks, and for conciseness, we write “Simulink blocks” to mean only the “time-driven Simulink blocks”.

We propose an approach for translating the behaviors of a Simulink diagram at (discrete) sample times to input/output-extended finite automata (I/O-EFA) (Kumar et al. 2006; Zhou and Kumar 2009). Note that a Simulink diagram can represent a hybrid system that combines event-driven discrete and time-dependent continuous behaviors, whereas I/O-EFA is a model of a reactive untimed infinite state system. Yet, since we are only interested in capturing the behaviors of a Simulink diagram at sample times, an I/O-EFA model (which is untimed) suffices.

Simulink provides a library of blocks (such as transfer functions, discontinuities, math operations, logic and bit operations etc.), which can be interconnected in a hierarchical fashion to form an overall Simulink diagram. We consider the blocks in the Simulink library to be “atomic”, and formally define an atomic-block. Further we formulate two rules, namely connecting-rule and conditioning-rule, used in Simulink for building complex blocks by combining the simpler ones, and formally define a class of Simulink diagrams formed using these rules. This recursive view of defining the class of all Simulink diagrams leads to a recursive translation in form of I/O-EFA.

In order to obtain an I/O-EFA model recursively, we first present an algorithm for translating an atomic-block to an I/O-EFA. Next for each rule of combining simpler Simulink diagrams to construct a complex Simulink diagram, we develop a corresponding rule for combining the I/O-EFA models of simpler Simulink diagrams to build the I/O-EFA model of the more complex Simulink diagram.

We introduce the concept of a step of an I/O-EFA to emulate the computation of a Simulink diagram at a sample time. A sequence of steps, namely, a step-trajectory, generates outputs over a sequence of sample times. We show that the translation approach is sound and complete: The input-state-output behavior of the I/O-EFA, 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).

The contributions of the work include:

• The translation approach is recursive. Formal definitions of an atomic Simulink block and a class of Simulink diagrams formed using the identified connecting-rule and conditioning-rule are provided. These definitions can be used to create a more complex Simulink diagram from the simpler ones.

• The model of I/O-EFA is amenable to automated test generation (Lee and Yannakakis 1996) or verification (Takenaka et al. 2006). The model can be directly supplied to a test generation or verification tool that accepts I/O-EFA models or programming languages such as C/C+ + or Java since an I/O-EFA model can be easily translated into these languages.

• The translation approach has no special restriction on the types of Simulink blocks. The approach supports virtually all blocks in Simulink Library (in this paper we only consider time-driven blocks) provided that the block can be mathematically written as input-state-output functions over time. Also unlike Agrawal et al. (2004), it does not require a clear separation between discrete and continuous dynamics for modeling hybrid systems. As an illustration, consider for example the bouncing ball example presented in the paper.

• 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).

• The translation approach can handle the Simulink features such as multi-rate diagrams, sample times with initial offsets, variable-step simulation etc.

• The translation approach is general in that it can be applied to other graphical modeling and simulation tools such as LabView.

2 I/O-EFA

We present the notion of an input-output extended finite automaton (I/O-EFA) as a formal model of representation for a Simulink diagram. I/O-EFA is a model of a reactive untimed infinite state system in form of an automaton, extended with discrete variables such as inputs, outputs, and data. Using I/O-EFA as a model, many value-passing processes can be represented as finite graphs. An I/O-EFA consists of locations (i.e., symbolic-state), data (i.e., numeric-state), numeric-inputs, numeric-outputs, symbolic-inputs, symbolic-outputs, transitions, an initial location, initial data values, and a final location. The locations (symbolic-states) together with the data (numeric-states) form the state-space of a I/O-EFA. The locations are finite and form the vertices of the automaton graph. The edges of the graph represent transitions between the locations and are guarded by constraints over the data and the inputs. The occurrence of a transition triggers a data update and an output assignment.

Definition 1

An input/output extended finite automaton (I/O-EFA) is a tuple P = (L, D, U, Y, Σ, Δ, ℓ₀, D ₀, ℓ _m , E), where

• L is the set of locations (symbolic-states),

• D = D ₁ ×  ⋯  × D _n is the set of typed data (numeric-states),

• U = U ₁ ×  ⋯  × U _m is the set of typed numeric-inputs,

• Y = Y ₁ ×  ⋯  × Y _p is the set of typed numeric-outputs,

• Σ is the set of symbolic-inputs,

• Δ is the set of symbolic-outputs,

• ℓ₀ ∈ L is the initial location,

• $D_0\subseteq D$ is the set of initial-data values,

• ℓ _m  ∈ L is the final location, and

• E is the set of edges, and each e ∈ E is a 7-tuple, e = (o _e , t _e , σ _e , δ _e , G _e , f _e , h _e ), where

  • o _e  ∈ L is the origin location,

  • t _e  ∈ L is the terminal location,

  • σ _e  ∈ Σ ∪ {ϵ} is the symbolic-input,

  • δ _e  ∈ Δ ∪ {ϵ} is the symbolic-output,

  • $G_e\subseteq D\times U$ is the enabling guard (a predicate),

  • f _e : D × U → D is the data-update function,

  • h _e : D × U → Y is the output-assignment function.

Initially, P starts from the initial location ℓ₀ and an initial data value ${\bf d}_0\in D_0$. While at a certain state $(\ell,{\bf d})\in L\times D$, a transition e ∈ E such that o _e  = ℓ is enabled if the input σ _e arrives, and the data d and input u are such that the guard G _e (d, u) holds. Note when σ _e  = ϵ, the transition is enabled when only the guard G _e (d, u) holds; on the other hand when $G_e(D,U)={\tt True}$, then the transition is enabled when only σ _e arrives. An enabled transition can be executed. The execution of an enabled transition e at the state $(o_e, {\bf d})$ causes P to transit to the location t _e , the data value is updated to $f_e({\bf d}, {\bf u})$, the output variable is assigned the value $h_e({\bf d}, {\bf u})$, and a discrete output δ _e is emitted.

3 Atomic-blocks: minimal Simulink diagrams

Simulink provides a library of blocks, which can be used as minimal systems, and the corresponding Simulink diagrams will then be minimal Simulink diagrams. We refer to such blocks as atomic blocks. The atomic-blocks can be composed in a recursive fashion to construct more complex Simulink diagrams, and we discuss the rules of composition in the next section.

An atomic-block can be stateful or stateless. A stateful block’s output depends on the history of its inputs. An example of a stateful block is the Unit Delay block. On the other hand, the output of a stateless block depends only on its current inputs. An example of a stateless block is the Gain block, which simply outputs its input signal, multiplied with a constant called the gain.

An atomic-block can be classified as continuous-time versus discrete-time, and is associated with a sample-period. For a continuous-time block, sample-period is the time between the instants when it is numerically simulated. For a discrete-time block, sample-period is the time between the instants when the corresponding discrete-time system evolves.

An atomic-block can be defined as follows.

Definition 2

An atomic Simulink block ψ can be represented as a tuple (U ^ψ, Y ^ψ, $D^\psi,D^\psi_0$, $\{(G_i^\psi,f_i^\psi,h_i^\psi)\}_{i=1}^{q^\psi}, (T^\psi,T^\psi_o))$, where

• $U^\psi=U_1^\psi\times \cdots\times U^\psi_{m^\psi}$ is the set of typed inputs,

• $Y^\psi=Y_1^\psi\times \cdots\times Y^\psi_{p^\psi}$ is the set of typed outputs,

• $D^\psi=D_1^\psi\times \cdots\times D^\psi_{n^\psi}$ is the set of typed data,

• $D^\psi_0\subseteq D^\psi$ is the set of initial data conditions,

• $\{(G^\psi_i, f^\psi_i,h^\psi_i)\}_{i=1}^{q^\psi}$ is a set of triples, where

  • $G^\psi_i\subseteq D^\psi\times U^\psi$ is a predicate representing an enabling guard, such that $\bigvee_{i=1}^{q^\psi}G_i$=True,

  • $f^\psi_i: D^\psi\times U^\psi\rightarrow D^\psi$ is a data-update function,

  • $h^\psi_i: D^\psi\times U^\psi\rightarrow Y^\psi$ is an output-assignment function.

• T ^ψ is the sample period and $T^\psi_o$ is an offset (it is assumed zero by default if unspecified).

Remark 1

The kth sampling time occurs at $kT^\psi+T^\psi_o$. The value of the input signal at the kth sampling time is denoted as ${\bf u}(k)=(u_1(k),...,u_{m^\psi}(k))\in U^\psi$, and similarly for other signals. At the kth sampling time, if the data d(k) and the input u(k) are such that $G^\psi_i({\bf d}(k),{\bf u}(k))$ holds, the next data, ${\bf d}(k+1)=f^\psi_i({\bf d}(k),{\bf u}(k))$, is computed, and the output value is assigned to ${\bf y}(k)=h^\psi_i({\bf d}(k),{\bf u}(k))$. Note that for continuous-time blocks, the data-update and output-assignment functions correspond to the ones obtained through discretization at sample times using an appropriate integration method. Simulink allows different kinds of sample period that include Discrete, Continuous, Inherited (−1), Constant (inf) and Triggered etc. Discrete sample periods are the only kind for which the evolution times of the corresponding system are known a priori. For blocks with other kinds of sample period, Simulink determines the evolution times of the corresponding system from the block’s type or by its context within the model during the compilation phase of simulation. Given a Simulink diagram, the sample period of a non continues-time block can be obtained from the get_param(object, ‘CompiledSampleTime’) command after compiling the diagram. The sample-period of a continuous-time block, which is used in discretization, can be chosen to be the greatest common divisor of all non continuous-time blocks using the following rule (Tripakis et al. 2005): for 1 ≤ i, j ≤ n, $T^\psi=\left\{\begin{array}{lll} gcd(\{T^{\psi_i}\}) & \mbox{ if } T^{\psi_i}_o=T^{\psi_j}_o\\ gcd(\{T^{\psi_i},T^{\psi_i}_o\}) & \mbox{ otherwise } \end{array}\right.$, and $^\psi_o=\left\{\begin{array}{lll} T^{\psi_i}_o & \mbox{ if } T^{\psi_i}_o=T^{\psi_j}_o\\ 0 & \mbox{ otherwise } \end{array}\right.$. Also note for a stateless atomic-block ψ, the set D ^ψ is empty (and accordingly, there are no initial data conditions or data-update functions).

The following example illustrates the Definition 2.

Example 1

The Integrator block provides a continuous-time integration of the input signal. It models the relations, $\dot d(t)=u(t)$ with d(0) = d ₀, and y(t) = d(t), where u is its input, d is its data, y is its output, t is the continuous-time variable, and d ₀ is the initial data condition. Using Euler’s Method the discretization is d(k + 1) = d(k) + T ^ψ u(k). Thus, the Integrator block can be represented as:

$$\big(u,y,d,d_0, \{(-,d(k+1)= d(k)+T^\psi u(k),y(k)=d(k))\}, (T^\psi,T^\psi_o)\big),$$

where T ^ψ is the sample-period and $T^\psi_o$ is an offset.

Note that the Integrator block can be configured further by setting certain parameters to have a more complex behavior. An example is the Integrator block ψ ₅ in Fig. 3. In Example 1 we did not include this much detail for the sake of simplicity of illustration.

We introduce the following concepts for the computation of an atomic block over sample times.

Definition 3

Given an atomic-block ψ and an input ${\bf u} \in U^\psi$, we call the computation of the corresponding output ${\bf y} \in Y^\psi$ a step of ψ over u. y is called the output of a step of ψ over u. Given an input sequence $\{{\bf u} (k)\}_{k=0}^K$, a step-trajectory of ψ over $\{{\bf u} (k)\}_{k=0}^K$ is a sequence of steps of ψ, where the kth step (0 ≤ k ≤ K) in the sequence is over the input u(k). Letting ${\bf y} (k) (0\leq k\leq K)$ denote the output of ψ over u(k), $\{{\bf y} (k)\}_{k=0}^K$ is called the output of step-trajectory of ψ over $\{u_k\}_{k=0}^K$.

4 System-blocks: Simulink diagrams

A Simulink diagram, also called a system-block, can be constructed by recursively composing atomic-blocks and other simpler system-blocks according to certain rules. The following two rules are the among the rules that Simulink uses for the construction of complex Simulink diagrams from the simpler ones:

• Connecting-rule: A certain input of one system-block can be connected to a certain output of another system-block. The connections over a set of system-blocks Ψ can be represented using a relation $C \subseteq (\Psi\times N)^2$, where N denotes the set of port numbers. A connection c = ((ψ ₁, i), (ψ ₂, j)) ∈ C connects the output port i of system-block ψ ₁ to an input port j of system-block ψ ₂. The “C-connected Ψ system” thus formed is denoted Ψ/C. Note a possible choice for connections is the“null-connection”, and {ψ}/ ∅ = ψ.

• Conditioning-rule: A system-block can be made conditionally executable when a certain guard condition over certain variables, called control-inputs, holds. Further the data may be reset when the guard condition holds, and the output may be reset when the guard condition is violated. Given a system-block ψ, a conditioning over ψ is a 5-tuple $\theta:=(U^\theta, G^\theta,f^\theta,h^\theta,(T^\theta,T^\theta_o))$, where

  • $U^\theta=U^\theta_1\times \cdots \times U^\theta_{m^\theta}$ is the set of conditioning-inputs (also called control-inputs),

  • $G^\theta\subseteq U^\theta$ is a condition (predicate) over U ^θ,

  • f ^θ: D ^ψ → D ^ψ is a data-resetting function,

  • h ^θ: Y ^ψ → Y ^ψ is an output-resetting function, and

  • T ^θ is a sample-period, $T^\theta_o$ is an offset.

  When G ^θ holds, ψ computes, and otherwise, h ^θ assigns the output. Also, when G ^θ becomes true, the first computation of ψ is preceded by a data-update by f ^θ. The “θ-conditioned ψ” system thus formed is denoted $\psi\!\!\Downarrow\!\!\theta$.

  The conditioning-rule can be implemented by placing a system-block inside a certain Subsystem block (of Simulink Library) which can be configured to specify the conditioning parameters. Note a possible choice for conditioning is “null-conditioning”, denoted $\bot:=(-,{\tt True},id,id,\infty)$, in which case $\psi\!\!\Downarrow\!\!\bot=\psi$. (Here id denotes the identity function.)

Next we formally define the class of Simulink diagrams (also referred to as system-blocks) formed using the above rules.

Definition 4

A certain class of Simulink diagrams (also referred to as system-blocks) is recursively defined as follows.

• 1. ψ is an atomic-block, then ψ is a system-block.

• 2. Ψ is a set of system-blocks, $C \subseteq (\Psi\times N)^2$ is a set of interconnections, then C-connected Ψ, denoted Ψ/C, is a system-block.

• 3. ψ is a system-block and θ is a conditioning over ψ, then θ-conditioned ψ, denoted $\psi\!\!\Downarrow\!\!\theta$, is a system-block.

Remark 2

For a system-block $\bar\psi:=\Psi/C$, we have:

• inputs $U^{\bar\psi}=\prod_{\not\exists ((\cdot,\cdot),(\psi,i))\in C} \ U^\psi_i$,

• outputs $Y^{\bar\psi}=\prod_{\psi\in \Psi} Y^{\psi}$,

• data $D^{\bar\psi}=\prod_{\psi\in \Psi} D^{\psi}$,

• initial data $D^{\bar\psi}_0=\prod_{\psi\in \Psi} D^{\psi}_0$, and

• sample-period $T^{\bar\psi}$ and offset $T^{\bar\psi}_o$ are obtained using the rule defined in Remark 1 over $\{T^\psi,T^\psi_o\mid\psi\in\Psi\}$.

Note the above definition of $T^{\bar\psi}$ ensures that each computation of each system-block ψ ∈ Ψ coincides with some computation of the connected system-block $\bar\psi$ (i.e., no computation of any system-block is missed).

Similarly, for a system-block $\bar\psi:=\psi\!\!\Downarrow\!\!\theta$, we have:

• inputs $U^{\bar\psi}=U^\psi\times U^\theta$,

• outputs $Y^{\bar\psi}=Y^\psi$,

• data $D^{\bar\psi}=D^{\psi}$,

• initial data $D^{\bar\psi}_0=D^{\psi}_0$,

• sample-period $T^{\bar\psi}\!=\! \left\{\begin{array}{ll} T^\theta\! & \!\mbox{if $T^\theta$ specif\/ied}\\ T^\psi\! & \!\mbox{otherwise} \end{array}\right.$, and offset $T^{\bar\psi}_o\; = \left\{\begin{array}{ll} T^\theta_o\! & \!\mbox{if $T^\theta$ specif\/ied}\\ T^\psi_o\! & \!\mbox{otherwise} \end{array}\right.$.

Note by the Simulink grammar, for a system-block $\bar\psi:=\psi\!\!\Downarrow\!\!\theta$, T ^θ is either specified and in which case $T^{\bar\psi}$ is inherited to be T ^θ, or is unspecified and in which case $T^{\bar\psi}$ is inherited to be T ^ψ. Similarly for $T^{\bar\psi}_o$.

Example 2

Consider the Simulink diagram ψ of a counter shown in Fig. 1, where the Unit Delay block ψ ₅ is a discrete-time atomic-block and the block ψ ₁ is a Enabled Subsystem block. The output y ₅ increases by 1 at each sample-period when the control input u is positive, and y ₅ resets to its initial value when the control input u is not positive. The Saturation block ψ ₂ limits the value of y ₅ in the range between −0.5 and 7. The sample-period of ψ ₅ is 0.01 s and others are either constant (inf) or inherited (−1). $T^{\psi_5}_o=0$ by default since unspecified. Using get_param command after compiling ψ, $T^\psi=T^{\psi_i}=0.01$ for i = 1, 2, 3, 4, 5. ψ belongs to the class of Simulink diagrams defined in Definition 4: ψ = {ψ ₁, ψ ₂}/C ₁, where

• $\psi_1=(\{\psi_3,\psi_4,\psi_5\}/C_2)\!\!\Downarrow\!\!\theta$, where

  • C ₂ = {((ψ ₃, ·), (ψ ₄, ·)), ((ψ ₄, ·), (ψ ₅, ·)), ((ψ ₅, ·), (ψ ₄, ·))},

  • θ = (U ^θ, u ^θ (k) > 0, d(k) = d ₀, (y ₃(k), y ₄(k), y ₅(k)) = (−, −, y ₅₀), −),

• C ₁ = {((ψ ₁, ·),(ψ ₂, ·))}, and

• ψ ₂, ψ ₃, ψ ₄, ψ ₅ are atomic-blocks.

Note since we choose the Pulse type of the source block Pulse Generator to be Time based, ψ is a single-rate Simulink diagram. Thus the source block for generating the inputs and the sink block Scope for displaying the outputs are not considered as part of the Simulink diagram being translated, and hence not included in ψ. If the Pulse type of the source block is chosen to be Sample based and the sample time is different from 0.01, then ψ becomes a multirate Simulink diagram.

Fig. 1

Simulink diagram of a counter

Example 3

Consider the multirate Simulink diagram ψ shown in Fig. 2, where blocks ψ ₃ and ψ ₇ are discrete-time blocks with sample-period of 0.01 and 0.025 s, respectively. The Zero-Order Hold block ψ ₈ is also a discrete-time block that samples the incoming signal at 0.01. Blocks ψ ₅ and ψ ₆ are continuous-time blocks. The sample-periods of other blocks are either constant (inf) or inherited (−1). All offsets are 0 by default since unspecified. Thus, $T^{\psi_i}=0.01$ for i = 1, 2, 3, 4, 8 and $T^{\psi_7}=0.025$. Since gcd(.01, .025) = .005, we opt to discretize ψ ₅ and ψ ₆ at a sample-period of .005. Then $T^{\psi_5}=T^{\psi_6}=0.005$, and also T ^ψ = 0.005.

Fig. 2

A multirate Simulink diagram

ψ belongs to the class of Simulink diagrams defined in Definition 4: ψ = Ψ/C, where Ψ = {ψ ₁, ψ ₂, ψ ₃, ψ ₄, ψ ₅, ψ ₆, ψ ₇, ψ ₈} and C is omitted. U = ∅, D = D ₃ × D ₅ × D ₆ × D ₇ with D ₀ = {(0, 0, 0, 0)}. Note the sink block Scope for displaying the outputs is not considered as part of the Simulink diagram being translated, and hence not included in ψ.

Example 4

Consider the Simulink diagram ψ of a bouncing ball shown in Fig. 3. ψ models a hybrid-system of a bouncing ball that is thrown up with an initial velocity of 15m/s from an initial height of 10m. y ₅ (resp., y ₂) is the position (resp., velocity) of the ball. ψ ₂ and ψ ₅ are continuous-time blocks. We have opted to discretize ψ ₂ and ψ ₅ at a sample period of .01. The sample-periods of other blocks are either constant (inf) or inherited (−1). Then $T^\psi=T^{\psi_i}=0.01$ for i = 1, ⋯ , 7. ψ belongs to the class of Simulink diagrams defined in Definition 4: ψ = Ψ/C, where Ψ = {ψ ₁, ψ ₂, ψ ₃,ψ ₄, ψ ₅, ψ ₆, ψ ₇} and C is omitted. U = ∅, D = D ₁ × D ₂ with D ₀ = {(15, 10)}.

Fig. 3

Simulink diagram of bouncing ball

4.1 Sorted-order

When system-blocks are composed using the connecting-rule to form a more complex system-block, the input of one system-block becomes the output of another system-block. To respect the interdependency of the inputs/outputs, Simulink defines and uses the notion of an execution-order (which it refers as sorted-order) to determine the order in which the system-blocks included inside a connected system-block are executed. Note that the conditioning-rule does not require defining a sorted-order since it is applied to a single system-block.

Given a system-block Ψ/C formed using the connecting-rule, the sorted-order of the system-blocks {ψ ∈ Ψ} is given as an ordering function $Ord:\Psi\rightarrow {\mathcal N}$, where $\mathcal N$ is the set of natural numbers. The sorted-order induces a total-order over Ψ, i.e., for ψ, ψ′ ∈ Ψ, Ord(ψ) = Ord(ψ′) if and only if ψ = ψ′. Accordingly ψ ∈ Ψ is executed before ψ′ ∈ Ψ if Ord(ψ) < Ord(ψ′). The sorted-order value Ord(ψ) can be displayed, as part of a label ascribed to a system-block ψ ∈ Ψ, by selecting the option Sorted Order from Simulink Block Displays menu. Assuming, without loss of generality of correctness of translation, that the Optimization on Conditional Execution Behaviors is turned off, the label ascribed to ψ has the format: Id(Ψ/C):Ord(ψ):{Id(ψ)}, where Id is a function that associates a certain identifier number to a system-block. The {Id(ψ)} part may be missing if ψ is an atomic-block. Whenever we need to indicate the label ascribed to ψ ∈ Ψ, we write it in the form: ψ[Id(Ψ/C):Ord(ψ){Id(ψ)}].

The notion of sorted-order is essential in defining the step of a system-block.

Definition 5

Given a system-block ψ and an input ${\bf u}\in U^\psi$, the step of ψ over u is recursively defined as follows:

• If ψ is an atomic-block, then the step of ψ over u is as defined in Definition 3.

• If ψ = Ψ/C is a connected system-block, then for j ^min ≤ j ≤ j ^max, where j ^min =  min {Ord(ψ) : ψ ∈ Ψ} and j ^max =  max {Ord(ψ) : ψ ∈ Ψ}, letting ψ _j  ∈ Ψ denote the system-block with Ord(ψ _j ) = j, a step of ψ over u is a sequence of steps, whose jth element is the step of ψ _j  ∈ Ψ over u _j , the input of ψ _j as determined by the set of connections C.

• If $\psi=\psi'\!\!\Downarrow\!\!\theta$ is a conditioned system-block, then a step of ψ over u is the step of ψ′ over u if G ^θ holds, and otherwise it is the execution of the output-resetting function h ^θ. Also when G ^θ becomes true, the first execution of the step of ψ′ over u is preceded by the execution of the data-resetting function f ^θ.

Given an input sequence $\{{\bf u} (k)\}_{k=0}^K$, a step-trajectory of ψ over $\{{\bf u} (k)\}_{k=0}^K$ is a sequence of steps of ψ, where the kth step (0 ≤ k ≤ K) in the sequence is over the input u(k). Letting ${\bf y} (k) (0\leq k\leq K)$ denote the output of ψ over u(k), $\{{\bf y} (k)\}_{k=0}^K$ is called the output of step-trajectory of ψ over $\{{\bf u}_k\}_{k=0}^K$.

Note in the 2nd item of Definition 5, when $kT^\psi+T^\psi_o=k^{\psi_j}T^{\psi_j}+T^{\psi_j}_o$, a step of ψ _j is computed by $h^{\psi_j}_i$ if $G^{\psi_j}_i$ holds, and $k^{\psi_j}$ increases when k increases; otherwise when $kT^\psi+T^\psi_o\neq k^{\psi_j}T^{\psi_j}+T^{\psi_j}_o$, the output of ψ _j remains its previous value, and $k^{\psi_j}$ remains unchanged when k increases.

Example 5

Consider the Simulink diagram ψ of the counter shown in Fig. 1 that was also discussed in Example 2, and its sorted-order displayed in Fig. 1. We have,

$$ \begin{array}{rll} \psi&=&\Psi_1/C_1=\{\psi_1\texttt{[0:1\{1\}]},\psi_2\texttt{[0:2]}\}/C_1,\\ \psi_1&=&(\Psi_2/C_2)\!\!\Downarrow\!\!\theta=(\{\psi_3\texttt{[1:0]},\psi_4\texttt{[1:2]}, \psi_5\texttt{[1:1]}\}/C_2)\!\!\Downarrow\!\!\theta. \end{array} $$

Then according to Definition 5 we have:

• A step of ψ = {ψ ₁, ψ ₂}/C ₁ is a step of ψ ₁ followed by a step of ψ ₂ since Ord(ψ ₁) = 1 < Ord(ψ ₂) = 2.

• A step of $\psi_1=(\{\psi_3,\psi_4,\psi_5\}/C_2)\!\!\Downarrow\!\!\theta$ is obtained as follows: If G ^θ holds, the sequence of steps of ψ ₃, ψ ₅, ψ ₄ is executed since Ord(ψ ₃) = 0 < Ord(ψ ₅) = 1 < Ord(ψ ₄) = 2; and otherwise, h ^θ computes. Also when G ^θ becomes true, the first execution of the sequence of steps of ψ ₃, ψ ₅, ψ ₄ is preceded by the computation of f ^θ.

Example 6

Consider the multirate Simulink diagram ψ of Fig. 2 that was also discussed in Example 3, and its sorted-order displayed in Fig. 2. It can be seen that

$$ \begin{array}{rll} \psi&=&\{\psi_1\texttt{[0:2]},\psi_2\texttt{[0:6]},\psi_3\texttt{[0:7]}, \psi_4\texttt{[0:8]},\psi_5\texttt{[0:3]},\\ &&\;\psi_6\texttt{[0:4]}, \psi_7\texttt{[0:0]}, \psi_8\texttt{[0:5]}\}/C. \end{array} $$

It then follows that a step of ψ is the sequence of steps of ψ ₇, ψ ₁, ψ ₅, ψ ₆, ψ ₈, ψ ₂, ψ ₃ and ψ ₄. Note for j = 1,  ⋯  , 8, a step of ψ _j is computed whenever $kT^\psi=k^{\psi_j}T^{\psi_j}$, and otherwise, ψ _j retains its previous values of the data and the output.

Example 7

Consider the Simulink diagram ψ of the bouncing ball of Fig. 3 that was also discussed in Example 4, and its sorted-order displayed in Fig. 3. It can be seen that

$$ \psi=\{\psi_1\texttt{[0:7]},\psi_2\texttt{[0:3]},\psi_3\texttt{[0:2]}, \psi_4\texttt{[0:1]},\psi_5\texttt{[0:5]},\psi_6\texttt{[0:4]},\psi_7\texttt{[0:0]}\}/C. $$

It then follows that a step of ψ is the sequence of steps of ψ ₇, ψ ₄, ψ ₃, ψ ₂, ψ ₆, ψ ₅ and ψ ₁.

5 Semantic translation of Simulink diagrams

We describe below our approach of how a Simulink diagram can be semantically translated to an I/O-EFA.

For any system-block ψ, its I/O-EFA model is obtained by connecting two I/O-EFA models, one for output-assignments and other for state-updates. We use $\ell_{0-}^\psi, \ell_{m-}^\psi$ to denote the initial/final location for first I/O-EFA, and $\ell_{0+}^\psi,\ell_{m+}^\psi$ to denote the initial/final location for second I/O-EFA. The two I/O-EFA’s are connected using two edges:

• succession-edge connecting the final location $l_{m-}^\psi$ of the first I/O-EFA to the initial location $l_{0+}^\psi$ of the second I/O-EFA, and

• time-advancement edge connecting the final location $l_{m+}^\psi$ of the second I/O-EFA to the initial location $l_{0-}^\psi$ of the first I/O-EFA that increments time: k : = k + 1.

Translating atomic-blocks

Figure 4 depicts the two I/O-EFA models connected by the succession and time-advancement edges for an atomic-block ψ. A formal description of the translation is provided in the following algorithm.

Fig. 4

I/O-EFA model of atomic-block ψ

Algorithm 1 For an atomic-block $\psi\!=\!(U^\psi,\!Y^\psi,\!D^\psi,\!D^\psi_0, \{(G_i^\psi,\!f_i^\psi,\!h_i^\psi)\}_{i=1}^{q^\psi}, (T^\psi,\!T^\psi_o))$,

• The 1st I/O-EFA of ψ is $P^{\psi}_-=(L^{\psi}_-, -$, U ^ψ, Y ^ψ, − ,  −, $\ell^{\psi}_{0-}, -,\ell^\psi_{m-}, E^{\psi}_-)$, where

  • $L^\psi_-=\{\ell^\psi_{0-},\ell^\psi_{m-}\}$, and

  • $E^\psi_-=\{(\ell^\psi_{0-},\ell^\psi_{m-},-,-,G^\psi_i,-,h^\psi_i)\mid i\leq q^\psi\}$.

• The 2nd I/O-EFA of ψ is $P^{\psi}_+=(L^{\psi}_+, D^{P^\psi}$, U ^ψ, Y ^ψ, − , −, $\ell^{\psi}_{0+}, D^{P^\psi}_{0}, \ell^\psi_{m+}, E^{\psi}_+)$, where

  • $L^\psi_+=\{\ell^\psi_{0+},\ell^\psi_{m+}\}$,

  • $D^{P^\psi}:=D^\psi\times K$ is the set of data, where K is the set of sampling times,

  • $D^{P^\psi}_{0}:=D^\psi_{0}\times \{0\}$ is the set of initial-data conditions, and

  • $E^\psi_+=\{(\ell^\psi_{0+},\ell^\psi_{m+},-,-,G^\psi_i,f^\psi_i,-)\mid i\leq q^\psi\}$.

  Note that $f^\psi=\mbox{ ``nul''}$ if ψ is a stateless block.

• The combined I/O-EFA model of ψ is $P^{\psi}=(L^{\psi}, D^{P^\psi}$, U ^ψ, Y ^ψ, − , −, $\ell^{\psi}_0, D^{P^\psi}_{0},\ell^\psi_m$, E ^ψ), where

  • $L^\psi=L^\psi_-\cup L^\psi_+$,

  • $\ell^\psi_0=\ell^\psi_{0-}$,

  • $\ell^\psi_m=\ell^\psi_{m+}$, and

  • $E^\psi=E^\psi_-\cup E^\psi_+$ ∪ $\{(\ell^\psi_{m-},\ell^\psi_{0+},-,-,-,-,-)\}$ ∪ $\{(\ell^\psi_{m+},\ell^\psi_{0-},-,-,-,-,$ k = k + 1)}.

Translating for connecting-rule

In the I/O-EFA models of a connected system-block $\bar\psi=\Psi/C$, the initial and final locations of the first (resp., second) I/O-EFA are the initial and final locations of the first (resp., second) I/O-EFA model of ψ ∈ Ψ that has the smallest and largest Ord(ψ)-value in Ψ, respectively. Also in order to preserve the sorted-order, there is an edge from the final location of the first (resp., second) I/O-EFA of ψ ∈ Ψ to the initial location of the first (resp., second) I/O-EFA of ψ′ ∈ Ψ if and only if Ord(ψ′) = Ord(ψ) + 1. Also in order to allow multirate system-blocks within a connected system-block, certain “bypass” edges are introduced within each system-block ψ ∈ Ψ connecting the initial location $\ell_{0-}^\psi$ (resp., $\ell_{0+}^\psi$) and final location $\ell_{m-}^\psi$ (resp., $\ell_{m+}^\psi$) of the first (resp., second) I/O-EFA of ψ. These edges are guarded by $[kT^{\bar\psi}+T^{\bar\psi}_o\neq k^{\psi}T^\psi+T^\psi_o]$, implying that ψ will be bypassed at those values of k when $kT^{\bar\psi}+T^{\bar\psi}_o$ is not equal to $k^{\psi}T^\psi+T^\psi_o$. In contrast, the converse guard condition of $[kT^{\bar\psi}+T^{\bar\psi}_o= k^{\psi}T^\psi+T^\psi_o]$ is introduced for the original set of edges originating at $\ell_{0-}^\psi$ and $\ell_{0+}^\psi$. An illustration of the translating of $\bar\psi=\Psi/C$ is depicted in Fig. 5, whereas a formalization is presented in Algorithm 2.

Fig. 5

I/O-EFA model of system-block $\bar\psi=\Psi/C$

Without loss of generality, we assume that if ((ψ, i), (ψ,j)) ∈ C, then $y_i^\psi=u_j^\psi$, i.e., the same variable has been used to denote the two signals.

Algorithm 2 For a connected system-block $\bar\psi=\Psi/C$,

• The 1st I/O-EFA of $\bar\psi$ is $P^{\bar\psi}_- = (L^{\bar\psi}_-, D^{P^{\bar\psi}}_-, U^{\bar\psi}, Y^{\bar\psi}$, − , −, $\ell^{\bar\psi}_{0-}, D^{P^{\bar\psi}}_{0-}, \ell^{\bar\psi}_{m-}, E^{\bar\psi}_-)$, where

  • $L^{\bar\psi}_-:=\cup_{\psi\in \Psi} L^\psi_-$,

  • $D^{P^{\bar\psi}}_-:=K\times \prod_{\psi\in\Psi} K^\psi\times T^{\bar\psi}\times T^{\bar\psi}_o\times \prod_{\psi\in\Psi} T^\psi\times \prod_{\psi\in\Psi} T^\psi_o$,

  • $U^{\bar\psi}$ and $Y^{\bar\psi}$ are as defined in first part of Remark 2,

  • $\ell^{\bar\psi}_{0-}=\ell^{\psi}_{0-}$ such that $Ord(\psi)=\mbox{min}\{Ord(\psi):\psi\in \Psi\}$,

  • $D^{P^{\bar\psi}}_{0-}= \{0\}\times \prod_{\psi\in\Psi} \{0\}\times T^{\bar\psi}\times T^{\bar\psi}_o\times \prod_{\psi\in\Psi} T^\psi\times \prod_{\psi\in\Psi} T^\psi_o$,

  • $\ell^{\bar\psi}_{m-}:=\ell^{\psi}_{m-}$ such that $Ord(\psi)=\mbox{max}\{Ord(\psi):\psi\in \Psi\}$, and

  • $E^{\bar\psi}_- {\kern-.3pt} = \bigcup_\psi \{(\ell^\psi_{0-},\ell^\psi_{m-},-,-,[kT^{\bar\psi}{\kern-.3pt}+{\kern-.3pt}T^{\bar\psi}_o{\kern-.3pt}={\kern-.3pt} k^{\psi}T^\psi{\kern-.3pt}+{\kern-.3pt}T^\psi_o]\wedge G^\psi_i,-,h^\psi_i)\mid i{\kern-.3pt}\leq{\kern-.3pt} q^\psi\}$

            ${\bigcup}_{\psi}\{(\ell^\psi_{0-},\ell^\psi_{m-},-,-, kT^{\bar\psi}+T^{\bar\psi}_o\neq k^{\psi}T^\psi+ T^\psi_o], -, {\bf y}^\psi(k)= {\bf y}^\psi(k-1))\}$

            $\bigcup \{(\ell^{\psi}_{m-},\ell^{\psi'}_{0-},-,-,-,-,-)\mid Ord(\psi')= Ord(\psi)+1\leq |\Psi|$, and ψ, ψ′ ∈ Ψ}.

• The 2nd I/O-EFA of $\bar\psi$ is $P^{\bar\psi}_+ = (L^{\bar\psi}_+, D^{P^{\bar\psi}}_+, U^{\bar\psi}, Y^{\bar\psi}$, − , −, $\ell^{\bar\psi}_{0+}, D^{P^{\bar\psi}}_{0+}, \ell^{\bar\psi}_{m+}, E^{\bar\psi}_+)$, where

  • $L^{\bar\psi}_+:=\cup_{\psi\in \Psi} L^\psi_+$,

  • $D^{P^{\bar\psi}}:= D^{\bar\psi} \times K\times \prod_{\psi\in\Psi} K^\psi\times T^{\bar\psi}\times T^{\bar\psi}_o\times \prod_{\psi\in\Psi} T^\psi\times \prod_{\psi\in\Psi} T^\psi_o$, where $D^{\bar\psi}$ is as defined in first part of Remark 2,

  • $U^{\bar\psi}$ and $Y^{\bar\psi}$ are as defined in first part of Remark 2,

  • $\ell^{\bar\psi}_{0+}=\ell^{\psi}_{0+}$ such that $Ord(\psi)=\mbox{min}\{Ord(\psi):\psi\in \Psi\}$,

  • $D^{P^{\bar\psi}}_{0+}= D^{\bar\psi}_{0} \times \{0\}\times \prod_{\psi\in\Psi} \{0\}\times T^{\bar\psi}\times T^{\bar\psi}_o\times \prod_{\psi\in\Psi} T^\psi\times \prod_{\psi\in\Psi} T^\psi_o$, where $D^{\bar\psi}_0$ is as defined in first part of Remark 2,

  • $\ell^{\bar\psi}_{m+}:=\ell^{\psi}_{m+}$ such that $Ord(\psi)=\mbox{max}\{Ord(\psi):\psi\in \Psi\}$, and

  • $E^{\bar\psi}_+= \bigcup_\psi \{(\ell^\psi_{0+},\ell^\psi_{m+},-,-, [kT^{\bar\psi}+T^{\bar\psi}_o=k^{\psi}T^\psi+T^\psi_o]\wedge G^\psi_i,({\bf d}^\psi(k+1), k^\psi)=$ $(f^\psi_i,k^\psi+1),-)\mid i\leq q^\psi\}$

               ${\bigcup}_{\psi}\{(\ell^\psi_{0+},\ell^\psi_{m+},-,-, [kT^{\bar\psi}+T^{\bar\psi}_o\neq k^{\psi}T^\psi+T^\psi_o], {\bf d}^\psi(k+1)={\bf d}^\psi(k),-)\}$

               ${\bigcup} \{(\ell^{\psi}_{m+},\ell^{\psi'}_{0+},-,-,-,-,-)\mid Ord(\psi')= Ord(\psi)+1\leq |\Psi|, \mbox{ and }\psi,$ ψ′ ∈ Ψ}.

• The combined I/O-EFA of $\bar\psi$ is $P^{\bar\psi} = (L^{\bar\psi}, D^{P^{\bar\psi}}, U^{\bar\psi}, Y^{\bar\psi}$, − , −, $\ell^{\bar\psi}_{0}, D^{P^{\bar\psi}}_0, \ell^{\bar\psi}_{m}, E^{\bar\psi})$, where

  • $L^{\bar\psi}:=L^{\bar\psi}_- \cup L^{\bar\psi}_+$,

  • $D^{P^{\bar\psi}}:=D^{P^{\bar\psi}}_+$,

  • $\ell^{\bar\psi}_{0}=\ell^{\bar\psi}_{0-}$,

  • $D^{P^{\bar\psi}}_0 = D^{P^{\bar\psi}}_{0+}$;

  • $\ell^{\bar\psi}_{m}:=\ell^{\bar\psi}_{m+}$, and

  • $E^{\bar\psi}=E^{\bar\psi}_-\cup E^{\bar\psi}_+\cup \{(\ell^{\bar\psi}_{m-},\ell^{\bar\psi}_{0+},-,-,-,-,-)\}$ ∪ $\{(\ell_{m+}^{\bar\psi},\ell_{0-}^{\bar\psi},-,-,-,-,k=k+1)\}$.

Remark 3

If $\bar\psi$ is a single-rate system-block, then the I/O-EFA model of $\bar\psi=\Psi/C$ presented in Algorithm 2 can be simplified since in this case $T^{\bar\psi}=T^\psi$ and $T^{\bar\psi}_o=T^\psi_o$ for each ψ ∈ Ψ, and so $kT^{\bar\psi}+T^{\bar\psi}_o= k^{\psi}T^\psi+T^\psi_o$ for each k. Accordingly,

$$ \begin{array}{rll} E^{\bar\psi}_-&=&\textstyle \bigcup_\psi E^{\psi}_-\cup \{(\ell^{\psi}_{m-},\ell^{\psi'}_{0-},-,-,-,-,-)\mid Ord(\psi')\\ &&{\kern42pt} =Ord(\psi)+1\leq |\Psi|, \mbox{and }\psi,\psi'\in\Psi\}, \;\mbox{ and} \\ E^{\bar\psi}_+&=&\textstyle \bigcup_\psi E^{\psi}_+\cup \{(\ell^{\psi}_{m+},\ell^{\psi'}_{0+},-,-,-,-,-)\mid Ord(\psi')\\ &&{\kern42pt} =Ord(\psi)+1\leq |\Psi|, \mbox{ and }\psi,\psi'\in\Psi\}. \end{array} $$

Example 8

Consider Ψ₂/C ₂ = {ψ ₃, ψ ₄, ψ ₅}/C ₂ of Example 2, where Ord(ψ ₃) < Ord(ψ ₅) < Ord(ψ ₄). The I/O-EFA model for Ψ₂/C ₂, obtained using Algorithm 2 for the connecting-rule and Remark 3, is shown in Fig. 6. The dotted boxes contain the 1st/2nd I/O-EFAs of ψ ∈ Ψ₂, and also of Ψ₂/C ₂.

Fig. 6

I/O-EFA model of Ψ₂/C ₂ of Example 2

Example 9

Consider the multirate Simulink diagram of Fig. 2 that was discussed in Example 3. The I/O-EFA model of ψ, obtained using Algorithm 2 for the connecting-rule, is shown in Fig. 7.

Fig. 7

I/O-EFA model of multirate Simulink diagram of Example 3

Translating for conditioning-rule

In the translation of a conditioned system-block $\bar\psi=\psi\!\!\Downarrow\!\theta$, the 1st I/O-EFA of $\bar\psi$ is the 1st I/O-EFA of ψ together with (i) a newly added location $\ell_{0-}^{\bar\psi}$, that also serves as the initial location of the first I/O-EFA model of $\bar\psi$, (ii) two newly added edges for capturing the conditional execution of ψ, and (iii) a “bypass edge” when the condition G ^θ doesn’t hold. The 2nd I/O-EFA of $\bar\psi$ is the 2nd I/O-EFA of ψ together with (i) a newly added location $\ell_{0+}^{\bar\psi}$, that also serves as the initial location of the second I/O-EFA model of $\bar\psi$, (ii) a newly added edge for capturing the conditional execution of ψ, and (iii) a “bypass edge” when the condition G ^θ doesn’t hold. An extra binary-valued data-variable d ^θ, with initial value 0, is introduced to keep track of the period over which G ^θ holds. An illustration of the translating of $\bar\psi=\psi\!\!\Downarrow\!\!\theta$ is depicted in Fig. 8, whereas a formalization is presented in Algorithm 3.

Fig. 8

I/O-EFA model of system-block $\bar\psi=\psi\Downarrow\theta$

Algorithm 3 For a conditioned system-block $\bar\psi=\psi\Downarrow\theta$,

• The 1st I/O-EFA model of $\bar\psi$ is $P^{\bar {\psi}}_- = (L^{\bar {\psi}}_-, D^\theta, U^{\bar {\psi}}, Y^{\bar {\psi}}$, − , −, $\ell^{\bar {\psi}}_{0-}, D^\theta_0, \ell^{\bar {\psi}}_{m-}, E^{\bar {\psi}}_-)$, where

  • $L^{\bar {\psi}}_-=L^\psi_-\cup \{\ell^{\bar {\psi}}_{0-}\}$,

  • D ^θ = {0,1},

  • $U^{\bar\psi}$ and $Y^{\bar\psi}$ are as defined in second part of Remark 2,

  • $D^\theta_0=\{0\}$,

  • $\ell^{\bar\psi}_{m-}=\ell^{\psi}_{m-}$, and

  • $E^{\bar\psi}_-=E^{\psi}_-$ ∪ $\{(\ell^{\bar\psi}_{0-},\ell^\psi_{0-}, -,-,G^\theta\wedge [d^\theta=0],(f^\theta;d^\theta:=1),-)\}$ ∪ $\{(\ell^{\bar\psi}_{0-}, \ell^\psi_{0-}$, − , −, G ^θ ∧ [d ^θ = 1], − , − )} ∪ $\{(\ell^{\bar\psi}_{0-}, \ell^\psi_{m-}$, − , −,$\neg G^\theta$,− ,h ^θ)}.

• The 2nd I/O-EFA model of $\bar\psi$ is $P^{\bar\psi}_+ = (L^{\bar\psi}_+, D^{P^{\bar\psi}}, U^{\bar\psi}, Y^{\bar\psi}$, − , −, $\ell^{\bar\psi}_{0+}, D^{P^{\bar\psi}}_0, \ell^{\bar\psi}_{m+}, E^{\bar\psi}_+)$, where

  • $L^{\bar\psi}_+=L^\psi_+\cup \{\ell^{\bar\psi}_{0+}\}$,

  • $D^{P^{\bar\psi}}=D^{P^\psi}\times D^\theta$,

  • $D^{P^{\bar\psi}}_0=D^{P^\psi}_0\times D^\theta_0$,

  • $\ell^{\bar\psi}_{m+}=\ell^\psi_{m+}$, and

  • $E^{\bar\psi}_+=E^\psi_+$ ∪ $\{(\ell^{\bar\psi}_{0+},\ell^\psi_{0+},-,-,G^\theta,-,-)\}$ ∪ $\{(\ell^{\bar\psi}_{0+},\ell^\psi_{m+},-,-,\neg G^\theta,({\bf d}^\psi(k+1),d^\theta)=({\bf d}^\psi(k),0),-)\}$.

• The combined I/O-EFA model of $\bar\psi$ is $P^{\bar\psi} = \big(L^{\bar\psi}, D^{P^{\bar\psi}}, U^{\bar\psi}, Y^{\bar\psi}$, − , −, $\ell^{\bar\psi}_0, D^{P^{\bar\psi}}_0, \ell^{\bar\psi}_m, E^{\bar\psi}\big)$, where

  • $L^{\bar\psi}=L^{\bar\psi}_-\cup L^{\bar\psi}_+$,

  • $\ell^{\bar\psi}_0=\ell^{\bar\psi}_{0-}$,

  • $\ell^{\bar\psi}_m=\ell^{\psi}_{m+}$, and

  • $E^{\bar\psi}=E^{\bar\psi}_-\cup E^{\bar\psi}_+$ ∪ $\{(\ell^\psi_{m-},\ell^{\bar\psi}_{0+},-,-,-,-,-)\}$ ∪ $\{(\ell^\psi_{m+},\ell^{\bar\psi}_{0-},-,-,-,-,k=k+1)\}$.

Remark 4

Algorithms 1, 2 and 3 provide translation under the fixed-step simulation semantics of Simulink. The algorithms can be modified to follow the variable-step simulation semantics as well. The variable-step solvers in the Simulink dynamically increase (or reduce) the step size (i.e., the value of $T^{\bar\psi}$) if the error exceeds (or falls under) a specific limit Er _ceiling (or Er _floor). To see the modification, suppose the error calculation formula is $f_e({\bf y}^{\bar\psi}(k), {\bf y}^{\bar\psi}(k-1), \cdots, T^{\bar\psi})$. Then the time-advancement edge $(\ell^\psi_{m+},\ell^{\bar\psi}_{0-},-,-,-,-,k=k+1)$ will be replaced by the following set of edges:

$$ \begin{array}{rll} \{(\ell^\psi_{m+},\ell^{\bar\psi}_{0-},-,-,[f_e>Er_{\rm ceiling}],T^{\bar\psi}=T^{\bar\psi}/2,k=k+1),\\ (\ell^\psi_{m+},\ell^{\bar\psi}_{0-},-,-,[f_e<Er_{\rm f\/loor}],T^{\bar\psi}=2*T^{\bar\psi},k=k+1),\nonumber\\ (\ell^\psi_{m+},\ell^{\bar\psi}_{0-},-,-,[Er_{\rm f\/loor}<f_e<Ef_{\rm ceiling}],-,k=k+1)\}. \end{array} $$

Example 10

Consider $\psi_1=(\Psi_2/C_2)\!\!\Downarrow\!\theta$ of Example 2. The I/O-EFA model of Ψ₂/C ₂ was obtained in Example 8, and the I/O-EFA model of ψ ₁, obtained using Algorithm 3 for the conditioning-rule, is shown in Fig. 9. The dotted boxes contain the 1st/2nd I/O-EFAs of Ψ₂/C ₂, and also of ψ ₁.

Fig. 9

I/O-EFA model of ψ ₁ of Example 2

Example 11

Consider the Simulink diagram ψ = {ψ ₁, ψ ₂}/C of the counter shown in Fig. 1 that was also discussed in Example 2. The I/O-EFA model for ψ ₁ was obtained in Example 10, and the I/O-EFA model of ψ, obtained using Algorithm 2 for the connecting-rule and Remark 3, is shown in Fig. 10.

Fig. 10

I/O-EFA model of counter of Example 2

Consider the Simulink diagram ψ of the bouncing ball of Fig. 3, and also discussed in Example 4. The I/O-EFA model of ψ, obtained using Algorithm 2 for the connecting-rule and Remark 3, is shown in Fig. 11.

Fig. 11

I/O-EFA model of bouncing ball of Example 4

6 Validation of translating approach

In order to show that the translating approach is sound and complete, we introduce the concept of a step and of a step-trajectory of an I/O-EFA model of a system-block. In the I/O-EFA model P ^ψ of a system-block ψ, each increment of k corresponds to an execution of a path $\pi=(\ell_0^\psi,\cdots, \ell_m^\psi, \ell_0^\psi)$. A computation along the kth execution of such a path gives an output value y(k) for an input u k.

Definition 6

Given an I/O-EFA model P ^ψ of a system-block ψ and input ${\bf u}\in U^\psi$, a step of P ^ψ over u is the computation of a sequence of edges starting from $\ell_0^\psi$ and ending at $\ell_m^\psi$, followed by the time-advancement edge. Given an input sequence $\{{\bf u} (k)\}_{k=0}^K$, a step-trajectory of P ^ψ over $\{{\bf u}(k)\}_{k=0}^K$ is a sequence of steps, where the kth step (0 ≤ k ≤ K) in the sequence is over the input u(k). Letting ${\bf y}(k) (0\leq k\leq K)$ denote the output of ψ over u(k), $\{{\bf y}(k)\}_{k=0}^K$ is called the output of step-trajectory of P ^ψ over $\{{\bf u}_k\}_{k=0}^K$.

Next we show that the input-output behavior of an I/O-EFA model at a sampling time, defined in terms of a step, preserves the input-output behavior of the corresponding Simulink diagram at the same sampling time, defined in terms of a step.

Lemma 1

Given a system-block ψ and an input u(k) and at the kth sampling time, let ${\bf y}^\psi(k)$ and ${\bf y}^{P^\psi}(k)$ be the outputs of the steps of ψ and P ^ψ, respectively, over u(k). Then ${\bf y}^\psi(k)={\bf y}^{P^\psi}(k)$, where P ^ψ is obtained from the Algorithms 1, 2 and 3.

Proof

If ψ is an atomic-block, then from Algorithm 1 and Definitions 5 and 6, a step of both ψ and P ^ψ at the kth sampling time k compute: ${\bf y}^\psi(k)=h^\psi_i({\bf d}(k),{\bf u}(k)), \mbox{ where }$

• $$ {\bf d}(k)=\left\{\begin{array}{ll} f^\psi_i({\bf d}(k-1),{\bf u}(k-1)) & \mbox{ if } k>0 \\ {\bf d}_0 & \mbox{ otherwise} \end{array}\right\} ,$$

  if $G^\psi_i({\bf d}(k),{\bf u}(k))$ holds, and

• i ≤ q ^ψ.

If ψ = Ψ/C, then from Algorithms 2 and Definitions 5 and 6, a step of both ψ and P ^ψ over u(k) at the kth sampling time compute $({\bf y}^{\psi_{j^{{\kern.9pt}\rm min}}}(k),\ldots,{\bf y}^{\psi_j}(k),\ldots{\bf y}^{\psi_{j^{{\kern.9pt}\rm max}}}(k))$, where ψ _j  ∈ Ψ and:

• (i) If $kT^\psi+T^\psi_o=k^{\psi_j}T^{\psi_j}+T^{\psi_j}_o$: ${\bf y}^{\psi_j}(k)=h^{\psi_j}_i({\bf d}(k),{\bf u}(k)), \mbox{ where }$

  • $$ {\bf d}(k)=\left\{\begin{array}{ll} f^{\psi_j}_i({\bf d}(k-1),{\bf u}(k-1)) & \mbox{if } k>0 \\ {\bf d}_0 & \mbox{otherwise} \end{array}\right\} ,$$

    if $G^{\psi_j}_i({\bf d}(k),{\bf u}(k))$ holds,

  • $i\leq q^{\psi_j}$, and

  • $u_r^{\psi_j}(k)=y_s^{\psi_{j'}}(k)$ if ((ψ _j ,r),(ψ _j′,s)) ∈ C.

• (ii) If $kT^\psi+T^\psi_o\neq k^{\psi_j}T^{\psi_j}+T^{\psi_j}_o$: ${\bf y}^{\psi_j}(k)={\bf y}^{\psi_j}(k-1).$

If $\bar\psi=\psi\Downarrow\theta$, then from Algorithms 3 and Definitions 5 and 6, a step of both ψ and P ^ψ over u(k) at the kth sampling time compute: ${\bf y}^{\bar\psi}(k)=\left\{\begin{array}{ll} h^\psi_i({\bf d}^\psi(k),{\bf u}^\psi(k)) & \mbox{if }G^\theta({\bf u}(k))\wedge G_i^\psi({\bf d}^\psi(k),{\bf u}^\psi(k)) \mbox{ holds, }\\ h^\theta({\bf d}^\psi(k),{\bf u}^\psi(k)) & \mbox{otherwise}, \end{array}\right\},$ where${\bf d}^\psi(k)=\left\{\begin{array}{ll} \left\{\begin{array}{ll} f^\theta({\bf d}^\psi(k-1),{\bf u}^\psi(k-1)) & \mbox{if } k>0\\ {\bf d}^\psi_0 & \mbox{otherwise} \end{array}\right\} & \mbox{if } G^\theta({\bf u}(k)) \mbox{ becomes true }\\ & \mbox{at the} k\mbox{th sampling time}\\ f^{\psi}_i({\bf d}^\psi(k-1),{\bf u}^\psi(k-1)) & \mbox{if } G^\theta({\bf u}(k)) \mbox{ remains true.}\\ \par \left\{\begin{array}{ll} {\bf d}^\psi(k-1) & \mbox{if } k>0 \\ {\bf d}^\psi_0 & \mbox{otherwise} \end{array}\right\} & \mbox{otherwise} \end{array}\right.$□

The following proposition shows that the input-output behavior of an I/O-EFA model over a sequence of sampling times, defined in terms of a step-trajectory, preserves the input-output behavior of the corresponding Simulink diagram over the same sequence of sampling times, defined in terms of a step-trajectory.

Proposition 1

Given a system-block ψ and an input sequence $\{{\bf u}(k)\}_{k=0}^K$, let $\{{\bf y}^{\bar\psi}(k)\}_{k=0}^K$ and $\{{\bf y}^{P^{\bar\psi}}(k)\}_{k=0}^K$ be the outputs of step-trajectories of ψ and P ^ψ, respectively, over $\{{\bf u}(k)\}_{k=0}^K$. Then $\{{\bf y}^{\bar\psi}(k)\}_{k=0}^K=\{{\bf y}^{P^{\bar\psi}}(k)\}_{k=0}^K$, where $P^{\bar\psi}$ is as obtained from the Algorithms 1, 2 and 3.

Proof

The proof follows from Lemma 1 and Definitions 5 and 6. □

Example 12

To validate our model, a simulation for a certain input sequence (pulse with period 1.2 s and pulse width 25%) was obtained for the Simulink diagram ψ of Fig. 1 (using fixed-step discrete solver) and is shown in Fig. 12. The simulation of the I/O-EFA model P ^ψ was done in Stateflow. Since a step of P ^ψ is defined to be the execution of a cycle starting from and ending at the initial location and visiting the final location once, the sample-period for the Stateflow model of P ^ψ was scaled down by the length of the cycle (the number of locations of P ^ψ). The simulation result of P ^ψ (using fixed-step discrete solver) is also shown in Fig. 12.

Fig. 12

Simulation of counter of Example 2 and its I/O-EFA model in Fig. 10

A simulation was obtained for the multirate Simulink diagram ψ of Fig. 2 (using fixed-step continuous solver ode1 Euler) and is shown in Fig. 13. The simulation of the I/O-EFA model P ^ψ was done in Stateflow (note the computer can not check the equality of two floating numbers, one way to handle this is to duplicate the set of T ^ψs and $T^\psi_o$s, relabel and amplify them to make them integers). Recall T ^ψ = 0.005. The sample-period for the Stateflow model of P ^ψ was scaled down by the number of locations of P ^ψ. The simulation result of P ^ψ (using fixed-step discrete solver) is also shown in Fig. 13.

Fig. 13

Simulation of multirate Simulink diagram Example 3 and its I/O-EFA model in Fig. 7

A simulation was obtained for the Simulink diagram ψ of Fig. 3 (using fixed-step continuous solver ode1 Euler) and is shown in Fig. 14. The simulation of the I/O-EFA model P ^ψ was done in Stateflow. Recall the sample-period of ψ is 0.01. The sample-period for the Stateflow model of P ^ψ was scaled down by the number of locations of P ^ψ. The simulation result of P ^ψ (using fixed-step discrete solver) is also shown in Fig. 14.

Fig. 14

Simulation of bouncing ball of Example 4 and its I/O-EFA model in Fig. 11

7 Related work

We briefly introduce the works related to ours, discussing succinctly their features. Agrawal et al. (2004) presented a translation algorithm for converting a restricted subclass of S/S diagrams into a semantically equivalent hybrid automaton. For the subclass of S/S diagrams considered, there exists a clear separation between the discrete and the continuous dynamics: All mode changes are made through switches, and whose controlling variables are restricted to be the outputs of the Stateflow modules. In general, however, the discrete modes do not have to be determined by the output variables of the Stateflow modules, and switches do not have to be used to switch continuous dynamics. Our approach does not require a clear separation between discrete and continuous dynamics for modeling hybrid systems. Also our translation approach has no special restriction on the types of Simulink blocks. The approach supports virtually all blocks in Simulink Library (in this paper we only consider time-driven blocks) provided that the block can be mathematically written as input-state-output functions over time. Alur et al. (2008) described a translation scheme for deriving hybrid automata models from S/S models. However, no formal algorithms are provided. We presented formal algorithms for the translation. Tripakis et al. (2005), Caspi et al. (2003) and Scaife et al. (2004) describes a technique for translating discrete-time Simulink diagrams into Lustre programs. Lustre is a synchronous language and the translation is a mapping between elements of Simulink diagrams (for example, signals and atomic blocks) and Lustre programs (for example, flows and operators/nodes). The execution sequence of Simulink blocks in the Lustre programs is determined by Lustre compiler. Also only the discrete-time blocks are translated. In our approach, the execution sequence of Simulink blocks is directly captured in the I/O-EFA model. Also, our approach supports virtually all time-driven blocks in Simulink Library. Gadkari et al. (2007) mentioned a translation of S/S diagrams into the language of SAL (Sal 2010) for the purposes of test generation. However the details of the translation were not given. Jersak et al. (2000) reported translation of Simulink diagrams to a model of concurrent processes communicating with FIFO queues or registers, called a SPI model, in contrast to I/O-EFA model in our approach. There has also been work on code-generation for Simulink diagrams (Lublinerman and Tripakis 2008a; Lublinerman et al. 2009; Lublinerman and Tripakis 2008b). One emphasis is in intellectual property reuse (i.e., code reuse for a group of atomic blocks) and so their approach is modular. In contrast we focus on formal modeling of Simulink diagrams with the goal of providing models that are readily amenable for further analysis (verification, test-generation, etc.).

8 Conclusion

We presented a recursive approach for translating a class of Simulink diagrams as input/output-extended finite automata (I/O-EFA), which is amenable to automated test generation or verification. We treat the blocks in the Simulink library to be “atomic” and formulate two rules used in Simulink for building complex blocks by combining the simpler ones. We provided a recursive and formal definition for the class of Simulink diagrams formed using these rules.

We presented algorithms for (i) translating an atomic-block as an I/O-EFA, (ii) combining the I/O-EFA models of simpler Simulink diagrams to build the I/O-EFA model of a more complex Simulink diagram, constructed using certain rules of composition. We introduced the concept of a step (resp., step-trajectory) of an I/O-EFA to emulate the computation of a Simulink diagram at a sample time (resp., over a sequence of sample times). We showed that the translating approach is sound and complete: The input-output behavior of an I/O-EFA model, as defined in terms of a step-trajectory, preserves the input-output behavior of the corresponding Simulink diagram at each sample time (assuming the same integration method for any of the continuous blocks with dynamics). Finally, the translation approach has no specific restriction on the types of Simulink blocks or the structure of Simulink diagrams supported and can handle multirate Simulink diagrams, sample times with initial offsets and variable-step simulation etc.