A Two-Way Path Between Formal and Informal Design of Embedded Systems

Abstract

It is well known that informal simulation-based design of embedded systems has a low initial cost and delivers early results; yet it cannot guarantee the correctness and reliability of the system to be developed. In contrast, the correctness and reliability of the system can be thoroughly investigated with formal design, but it requires a larger effort, which increases the development cost. Therefore, it is desirable for a designer to move between formal and informal design. This paper describes how to translate Hybrid CSP (HCSP) formal models into Simulink graphical models, so that the models can be simulated and tested using a MATLAB platform, thus avoiding expensive formal verification if the development is at a stage where it is considered unnecessary. Together with our previous work on encoding Simulink/Stateflow diagrams into HCSP, it provides a two-way path in the design of embedded systems, so that the designer can flexibly shift between formal and informal models. The translation from HCSP into Simulink diagrams is implemented as a fully automatic tool, and the correctness of the translation is justified using Unifying Theories of Programming (UTP).

1 Introduction

Correct and efficient design of complex embedded systems is a grand challenge for computer science and control theory. Model-based design (MBD) is thought to be an effective solution. This approach begins with an abstract model of the system to be developed. Extensive analysis and verification of the abstract model are then performed so that errors can be identified and corrected at a very early stage. Then the higher-level abstract model is refined to step by step to more detailed models till a level where the system can be built with existing components or a few newly developed ones.

Many MBD approaches targeting embedded systems have been proposed and used in industry and academia. These approaches can be simulation-based informal ones such as Simulink/Stateflow [1, 2], Modelica [3], SysML [4], MARTE [5], or they can be verification based like Metropolis [6], Ptolemy [7], hybrid automata [8], CHARON [9], HCSP [10, 11], Differential Dynamic Logic [12], Hybrid Hoare Logic [13]. It is evident that informal design of embedded systems has a low initial cost and is intuitively appealing, because simulations give results early on, but it cannot fully guarantee the correctness and reliability of the system to be developed; in contrast, the correctness and reliability of the system can be thoroughly investigated with formal design, but the cost is higher and it requires specialized skills. Therefore, it is desirable to provide a two-way path between formal and informal approaches for a designer.

The first contribution of this paper is to provide one lane of this path. It takes a formal model and translates it automatically to a Simulink model. The other lane has been developed in previous work [14, 15]. The translation from the formal to informal model presented here, is implemented as a fully automatic tool. Another contribution of this paper is to provide a justification of the correctness of the translation. To this end, we define a UTP semantics for Simulink and a UTP semantics for HCSP, and then establish a correspondence between the two. Due to lack of space, the implementation and a case study on a lunar lander have been omitted and can be found in [16].

1.1 Related Work

There has been a range of works on translating Simulink/Stateflow into modelling formalisms supported by analysis and verification tools. Mathworks itself released a tool named Simulink Design Verifier [17] (SDV) for formal analysis of Simulink/Stateflow models. However, currently, SDV can only be used to detect low-level errors such as integer overflow, dead logic, array access violation, division by zero, and so on, in blocks of a model, but not system-level properties of the complete model with the physical and environmental aspects taken into account.

Simulation-based verification [18] can be used to verify system-level properties in a bounded time, but cannot be applied for unbounded verification. Thus there is work on translating Simulink into other modelling formalisms, for which analysis and verification tools are developed. Tripakis et al. [19] presented an algorithm of translating discrete-time Simulink models to Lustre, a synchronous language developed with formal semantics and a number of tools for validation and analysis, and later extended the work by incorporating a subset of Stateflow [20]. Cavalcanti et al. [21] presented a semantics for discrete-time Simulink diagrams using Circus [22], a combination of Z and CSP. Meenakshi et al. [23] gave an algorithm that translates a subset of Simulink intothe input language of model checker NuSMV. Sifakis et al. proposed a translation into BIP in [24]. BIP [25] stands for Behaviour, Interaction and Priority, which is a component-based formal model for real-time concurrent systems. These works do not consider continuous time models of Simulink. This is considered in the follpwing works. Yang and Vyatkin [26] translate Simulink into Function Blocks. Zhou and Kumar investigated how to translate Simulink into Input/Output Hybrid Automata [27], while the translation of both discrete and continuous time fragments of Simulink into SpacEx Hybrid Automata was considered in [28]. In [29], Chen et al. translates Simulink models to a real-time specification language Timed Interval Calculus (TIC). In this, continuous Simulink diagrams can be analyzed by a theorem prover. However, the translation is limited as it handles only continuous blocks whose outputs can be represented explicitly by a mathematical relation on inputs. In contrast, in [14] is a translation from Simulink into HCSP which handles all continuous blocks using the notion of differential equations and invariants.

Contract-based frameworks for Simulink are described in [30, 31]. In [30], Simulink diagrams are represented by SDF graphs, and discrete-time blocks are specified by contracts with pre/post-conditions. Then sequential code is generated from the SDF graph, and the code is verified using traditional refinement-based techniques. In [31], Simulink blocks are annotated with rich types, then the SimCheck tool extracts verification conditions from the Simulink model and the annotations, and submits them to an SMT solver for verification. While in our approach, all Simulink/Stateflow models can be specified and verified using Hybrid Hoare Logic and its deductive verification techniques.

In [32], a compositional formal semantics built on predicate transformers was proposed for Simulink, based on which, a tool for verification of Simulink blocks was reported in [33], consisting of two components: a translator from Simulink hierarchical block diagrams into predicate transformers and an implementation of the theory of predicate transformers in Isabelle. The UTP semantics of Simulink/Stateflow defined here is quite similar to the one given in [32].

There have been several formal semantics defined for HCSP. In He’s original work on HCSP [10], an algebraic semantics of HCSP was given. Subsequently, a Duration Calculus (DC) based semantics for HCSP was presented in [11]. These two original formal semantics of HCSP are very restrictive and incomplete, for example, it is unclear whether the set of algebraic rules defined in [10] is complete, and super-dense computations and recursion are not well handled in [11]. In [13, 34,35,36], operational, axiomatic and DC-based denotational semantics for HCSP are proposed, and the relations among them are discussed. In this paper, we re-investigate the semantics of HCSP by defining its simulation semantics using Simulink and its UTP-based denotational semantics, and study the correspondence between the two semantics.

The rest of this paper introduces HCSP and Simulink in Sect. 2, Sect. 3 presents the translation from HCSP into Simulink. Section 4 presents a justification of the translation by proving consistency of the UTP semantics. A conclusion is in Sect. 5.

2 Preliminaries

HCSP [10, 11, 34] is a language for describing hybrid systems. It extends the well-known language of Communicating Sequential Processes (CSP) with timing constructs, interrupts, and differential equations for modelling continuous evolution. Data exchange among processes is confined to instantaneous synchronous communication, avoiding shared variables between parallel processes.

Simulink [1] is an interactive platform for modelling, simulating and analyzing multidomain dynamic and embedded systems. It provides a graphical block diagramming tool and a customizable set of block libraries for building executable models.

2.1 Hybrid CSP (HCSP)

The syntax of HCSP processes is given below:

Here $x$ and $s$ stand for variables, $B$ and $e$ are conventional Boolean and arithmetic expressions. $P, Q, Q_i$ are sequential processes; and $io_i$ stands for a communication event, which is either $ch?x$ or $ch!e$, and $ch$ for a channel name. A system S is either a sequential process, or a parallel composition of several sequential processes.

The processes taken from CSP, $\text {skip}$, $x: = e$ (assignment), $ch?x$ (input), $ch!e$ (output), $P; Q$ (sequential composition), $B \rightarrow P$ (conditional statement), $P^*$ (repetition), $P \sqcup Q$ (internal choice), and $S\Vert S$ (parallel composition) have their standard meaning.

The evolution statement is $\langle {F}(\dot{s},s)=0 \& B\rangle$, where s represents a vector of real variables and $\dot{s}$ the first-order time derivative of s. It forces $s$ to evolve according to the differential equations defined by the functional ${\mathcal F}$ as long as $B$ holds, and it terminates immediately when B becomes false.

The process behaves like $\langle {F}(\dot{s},s)=0 \& B\rangle$, except that the evolution is preempted as soon as one of the communications $io_i$ occurs. That is followed by the respective $Q_i$. However, if the evolution statement terminates before a communication occurs, then the process terminates immediately.

2.2 Simulink

A Simulink model contains a set of blocks, subsystems, and wires, where blocks and subsystems cooperate by setting values on the wires between them. An elementary block gets input signals and computes the output signals. However, to make Simulink more useful, almost every block in Simulink contains some user-defined parameters to alter its functionality. One typical parameter is sample time which defines how frequently the computation is. done. Two special values, 0 and $-1$, may be set for sample time, where the sample time 0 indicates that the block is used for simulating the physical environment and hence computes continuously, and $-1$ signifies that the sample time of the block is not set, it will be determined by the sample times of the in-going wires to the block. Thus, blocks are classified into two categories, i.e. continuous and discrete, according to their sample times.

Blocks and subsystems in a Simulink model receive inputs and compute outputs in parallel, and wires specify the data flow between blocks and subsystems. Computation in a block takes no time and the output is delivered immediately to its receiver.

As a convention, in the sequel, when describing Simulink diagrams, we use x to stand for the input signal on in-port In_x, $x'$ for the output signal on out-port Out_x, possibly with a subscript to indicate which subsystem the signal belongs to. For instance, $x'_P$ indicates an output signal on Out_x inside a subsystem P.

3 From HCSP to Simulink

The translation from HCSP processes into graphical Simulink models starts from the most basic ingredients, i.e. expressions, to primitive statements and then is followed by compositional components.

3.1 Expressions

Arithmetic expressions in HCSP are translated to a normal subsystem in Simulink. A variable x is encoded into an input block of the subsystem, a constant c into a constant block with corresponding value, and parentheses determine priority of the computation. As for the operations over reals, a sequence of $+$ and − (or $*$ and  / ) is shrunk into a sum (or product) block with multiple input signals in Simulink. In the example for assignment in Fig. 3 is included the Simulink subsystem for the expression $x+y*z$. Boolean expressions are translated similarly.

Fig. 1.

$\dot{v}=1,\dot{s}=v+2$

Fig. 2.

$\text {skip}$ statement

3.2 Differential Equations

The syntax of differential equations in HCSP is $F ~ \widehat{=}~ \dot{s} = e \mid F , F$, where s stands for a continuous variable, $\dot{s}$ is the time derivative of s, and F, F indicates a group of differential equations that evolve simultaneously over time.

Each single differential equation is encoded into a continuous integrator block with an input signal of the value of e and an output signal of s; equations in the same group are a normal subsystem in Simulink. For example, $\dot{v}=1,\dot{s}=v+2$, becomes the block in Fig. 1, the integrator block of s takes the value of $v+2$ and an internal initial value $s_0$ to calculate the integral and then generate a signal of s, i.e. $s(t) = \int _{t_0}^t (v(t)+2)dt + s_0$.

3.3 skip Statement

In HCSP, $\text {skip}$ terminates immediately with no effect on the process, and thus there is intuitively no need to draw anything in Simulink diagrams. However, blocks and subsystems in a Simulink model are running inherently in parallel, but processes in HCSP can be executed sequentially, thus we need a mechanism to specify sequential execution in a Simulink diagram. Inspired by UTP [37], we introduce Boolean signals $\textit{ok}$ and $\textit{ok}'$ into each subsystem to represent initiation and termination. Whenever ${\textit{ok}'}$ is false, the process has not terminated and the final values of the process variables are unobservable. Similarly, when $\textit{ok}$ is false, the process has not started and even the initial values are unobservable. These conventions permit translation of sequential composition. Both $\textit{ok}$ and ${\textit{ok}'}$ are local to each HCSP process, and they never occur in expressions.

In a Simulink subsystem $\textit{ok}$ and ${\textit{ok}'}$ are given by an in-port In_ok and an out-port Out_ok respectively. Since $\text {skip}$ does nothing and terminates instantly, the subsystem for $\text {skip}$ in Simulink in Fig. 2 has , indicating that whenever $\text {skip}$ starts, it terminates immediately without any effect.

3.4 Assignment

Figure 3 illustrates the subsystem in Simulink with an example of assignment $x:=x+y*z$, where for ease of understanding, we unpack the subsystem of arithmetic expression e. The output signals are computed by the following equations:

$$\begin{aligned} \textit{ok}' = \textit{ok} \qquad x' = \left\{ \begin{array}{lll} x'_{\textit{new}}, &{} \textit{ok} \wedge \lnot d(\textit{ok}) \\ x, &{} \lnot \textit{ok} \wedge \lnot d(\textit{ok}) \\ d(x'), &{} d(\textit{ok}) \end{array} \right. \qquad \mathbf {u}' = \mathbf {u} \end{aligned}$$

Here, $\mathbf {u}$ stands for the set of signals that are not processed by the current subsystem, i.e. y and z in this example. $x'_{new}$ represents the newly computed signal, here produced by block Add1. Moreover, we use d(x) to denote the value of x in the previous period. It is kept through a unit delay block that holds its input for one period of the sample time.

Fig. 3.

$x:=x+y*z$

Fig. 4.

Continuous evolution

3.5 Continuous Evolution

The Simulink diagram translated from an evolution in HCSP is shown in Fig. 4, where the group of differential equations ${\mathcal F}$ and the Boolean condition B are encapsulated into a single subsystem respectively. The enabled subsystem F contains a set of integrator blocks corresponding to the vector s of continuous variables, and executes continuously whenever the value of the input signal, abbreviated as en, on the enable-port is positive. Intuitively, subsystem B guards the evolution of subsystem F by taking the output signals of F as its inputs, i.e. $s_B = s'_F$, and partially controlling the enable signal of F via its output Boolean signal, denoted by B. As a consequence, an algebraic loop occurs between subsystem B and F which is not allowed in Simulink, the simple solution is to introduce a unit delay block with an initial value 1 inserted after subsystem B. Thus the boundary condition is evaluated after completion of an integrator step. Formally, given inputs, the output signals are computed by the following equations:

$$\begin{aligned} en = \textit{ok} \wedge d(B) \qquad \textit{ok}' = \textit{ok} \wedge \lnot d(B) \qquad s' = \left\{ \begin{array}{ll} s'_F, \quad \textit{ok} \\ s, \quad \lnot \textit{ok} \end{array} \right. \end{aligned}$$

3.6 Conditional Statement

Figure 5 illustrates the translation from a conditional statement of HCSP into a Simulink diagram. In most cases, subsystem B and P share the same group of input signals x, and for those distinct input signals, we add corresponding in-ports for B or P, which is not presented in Fig. 5. Accordingly, the output signals are computed according to

$$\begin{aligned} \textit{ok}_P = \textit{ok} \wedge B \qquad \textit{ok}' = \left\{ \begin{array}{ll} \textit{ok}'_P, \quad B \\ \textit{ok}, \quad \lnot B \end{array} \right. \qquad x' = x'_P. \end{aligned}$$

3.7 Internal Choice

Given an internal choice $P \sqcup Q$, we use $\textit{outSigs}(\mathrm {P})$ and $\textit{outSigs}(\mathrm {Q})$ to represent the set of output signals (including $\textit{ok}'$) of subsystem P and Q respectively, and encode the random choice according to the following two situations.

• For each $x' \in \textit{outSigs}(\mathrm {P}) \cap \textit{outSigs}(\mathrm {Q})$, we introduce a switch block in Simulink diagrams for signal routing, which switches $x'$ between $x'_P$ from P and $x'_Q$ from Q based on the value of the second input.

• For each $y' \in \textit{outSigs}(\mathrm {P}) - \textit{outSigs}(\mathrm {Q})$, we directly output the signal $y'_P$ from P as the final value of $y'$, because in case that P is not chosen by the system, $y'$ stays unchanged. For each $z' \in \textit{outSigs}(\mathrm {Q}) - \textit{outSigs}(\mathrm {P})$, analogously.

Figure 6 illustrates a pattern to implement the above two cases. In order to guarantee that only one process in the internal choice is switched on, every switch block here needs to share exactly the same switching condition. As shown in Fig. 6, the two switch blocks share a common criteria ($>0$) for passing first input as well as an identical second input signal, abbreviated as $\textit{Ran}$, generated by an oracle that provides a non-deterministic signal¹. The computation of signal $\textit{ok}$ and $\textit{ok}'$ can be formalized as

$$\begin{aligned} \left\{ \begin{array}{ll} \textit{ok}_P = \textit{ok} \wedge \textit{Ran} \\ \textit{ok}_Q = \textit{ok} \wedge \lnot Ran \end{array} \right. \qquad \textit{ok}' = \left\{ \begin{array}{ll} \textit{ok}'_P, &{} Ran \\ \textit{ok}'_Q, &{} \lnot Ran \end{array} \right. \end{aligned}$$

Fig. 5.

Conditional statement

Fig. 6.

Internal choice

3.8 Sequential Composition

An essential work in translating sequential composition into Simulink models, is to construct the initiation and termination of a process, which has already been done by introducing $\textit{ok}$ and $\textit{ok}'$ signals in connection with the skip process.

Fig. 7.

Sequential composition

Figure 7 illustrates a straightforward encoding of sequential composition into Simulink diagrams. For exclusive signals y and z, we draw corresponding ports independently for subsystem P and Q. The set of common signals x processed by both P and Q is linked sequentially from P to Q, and the same happens for $\textit{ok}$ and $\textit{ok}'$.

$$\begin{aligned} \textit{ok}_P = \textit{ok} \quad \textit{ok}_Q = \textit{ok}'_P \quad \textit{ok}' = \textit{ok}'_Q \qquad x_P = x \quad x_Q = x'_P \quad x' = x'_Q \quad \end{aligned}$$

3.9 Repetition

The basic idea in encoding repetition is to link the outputs of subsystem P back into its in-ports, and we need to specify a finite random number N to control the number of times that P executes.

Fig. 8.

Repetition

The integrated pattern to encode repetition $p^*$ into Simulink diagrams is elaborated in Fig. 8. Here, a unit delay block with an initial value of 0 is introduced to break the algebraic loop that occurs when we link the outputs of P back. Besides, we introduce an oracle carrying a non-negative random number N to specify the number of repetitions of subsystem P. The update of variables is formulated as the following equations:

$$\begin{aligned} \begin{array}{ll} n = \textit{ok} \times (d(n) + d(\textit{ok}'_P \wedge \lnot d(\textit{ok}'_P))) \qquad \textit{ok}' = \textit{ok} \wedge \textit{ok}'_P \wedge (n \ge N) \\ \ \ \textit{ok}_P = \textit{ok} \wedge (n==d(n) \vee n \ge N) \qquad \ \; \quad x_P = \left\{ \begin{array}{ll} d(x'_P), n>0 \\ x, \ \ \ \ n==0 \end{array} \right. \end{array} \end{aligned}$$

3.10 Communication Events

For each communication event, either a sender ($\textit{ch}!e$) or a receiver ($\textit{ch}?x$), we construct a subsystem in Simulink to deliver the message along $\textit{ch}$ for the matching pair of events. In order to synchronise the interaction, we introduce another pair of Boolean signals $\textit{re}$ and $\textit{re}'$ ($\textit{re}$ is short for ready) into each subsystem that corresponds to a communication event. $\textit{re}$ indicates whether the matching event is ready for the communication, while $re'$ indicates whether the event itself is ready for the communication.

A communication along channel $\textit{ch}$ takes place as soon as both $\textit{re}_{\textit{ch}}$ and $\textit{re}'_{\textit{ch}}$ are true, then both the sending and the receiving parties are ready, otherwise one or both sides must wait. Additionally, $\textit{re}$ and $\textit{re}'$ are local signals, which never occur in the process statements. Furthermore, $\textit{re}$ and $\textit{re}'$ in a Simulink subsystem are constructed as an in-port signal named In_re and an out-port signal named Out_re respectively. Figure 9 illustrates the Simulink diagrams that interpret communication events, which can be elaborated in the following two parts.

Fig. 9.

Communication events

• For a sender $\textit{ch}!e$, the output signals are computed according to

  $$\begin{aligned} \textit{re}' = \textit{ok} \wedge \lnot \textit{ok}' \quad \textit{ok}' = f(d(\textit{re} \wedge \textit{re}')) \quad e' = \left\{ \begin{array}{ll} e, \quad \lnot d(\textit{ok}) \\ d(e'), \quad d(\textit{ok}) \end{array} \right. , \end{aligned}$$

  where the keep pattern $f(s(t)) = \textit{ok}(t) \wedge (s(t) \vee f(s(t-1)))$ for $t > \textit{cnow}$, with $f(s(\textit{t}))=0$ for $t\in [\textit{cnow}, \textit{cnow}+1)$, here $\textit{cnow}$ is the current time. This is to keep $\textit{ok}'$ true since the communication is finished, i.e., since both $\textit{re}$ and $\textit{re}'$ turn true.

• For a receiver $\textit{ch}?x$, the output signals are computed according to

  $$\begin{aligned} \begin{array}{ll} \textit{re}' = \textit{ok} \wedge \lnot \textit{ok}' \quad \textit{ok}' = f(d(\textit{re} \wedge \textit{re}')) \\ x' = \left\{ \begin{array}{ll} x, \quad \text{ if } \lnot \textit{ok}' \\ \lnot d(\textit{ok}') \times \textit{ch} + d(\textit{ok}') \times d(x'), &{} \text{ otherwise } \end{array} \right. \end{array} \end{aligned}$$

3.11 Parallel

For $P\Vert Q$, we consider the following two cases:

Without communications. This is a trivial case that we draw a subsystem encapsulating the two subsystems in terms of P and Q, but without any wires (except those carrying $\textit{ok}$, $\textit{ok}'$) between the two subsystems, as shared variables are not allowed in HCSP. Specifically, we set $\textit{ok}_P = \textit{ok}_Q = \textit{ok}$, and $\textit{ok}'= \textit{ok}'_P \wedge \textit{ok}'_Q$.

With communications. As for a parallel process $P \Vert Q$ with inter-communications along a set of common channels $\textit{comChan}(P,Q)$, we draw a subsystem containing the subsystems corresponding to P and Q, as well as some additional wires to bind all channels in $\textit{comChan}(P,Q)$ and deliver messages along them.

Fig. 10.

Parallel $e:=0;\textit{ch}!e;<\dot{e}=1 \& e<2>;\textit{ch}!e \Vert x:=3;\textit{ch}?x;\textit{ch}?x$

We elaborate the above idea by showing a Simulink diagram corresponding to a parallel process in Fig. 10, where the signals relevant to communications are attached with subscripts to specify the name of the common channel and the distinctive events corresponding to the same channel. Suppose that there are m and n events relevant to $\textit{ch}$ in subsystem P and Q respectively, then the computation in Fig. 10 is done by

$$\begin{aligned} \textit{ok}_P = \textit{ok}_Q = \textit{ok} \quad \textit{ok}'= \textit{ok}'_P \wedge \textit{ok}'_Q \quad \textit{re}_{\textit{ch}\_P} = \bigvee \nolimits _{i=1}^n \textit{re}'_{\textit{ch}\_i\_Q} \quad \textit{re}_{\textit{ch}\_Q} = \bigvee \nolimits _{j=1}^m \textit{re}'_{\textit{ch}\_j\_P} \end{aligned}$$

indicating that the two subsystems in parallel are activated simultaneously when the system starts, and the parallel process terminates when both P and Q terminate. Furthermore, the channel $\textit{ch}$ on one side claims ready to the other side if either of its involved events is ready, which means that the communication events on different parties of a common channel are matched dynamically during the execution. Moreover, the value that Q receives along channel $\textit{ch}$ is computed as $\textit{ch}_Q = \sum \nolimits _{j=1}^m \textit{re}'_{\textit{ch}\_j\_P} \times \textit{ch}'_{j\_P}$.

3.12 External Choice by Communications

As a subcomponent of interruption in HCSP, the external choice waits until one of the communications $io_i$ takes place, and then it is followed by the respective $Q_i$, where I is a non-empty finite set of indices, and $\{ io_i\}_{i\in I}$ are communication events, i.e. either $\textit{ch}!e$ or $\textit{ch}?x$. In addition, if more than one among $\{io_i\}_{i\in I}$ are ready simultaneously, only one of them executes, this is determined randomly by the system. Thus, if the matching side of every $io_i$ involved is ready for communication, then the external choice degenerates to internal choice. Besides, the syntax $(io_i \rightarrow Q_i)$ actually indicates a sequential composition $(io_i \rightarrow \text {skip}~; Q_i)$, to which the translation approach already has been introduced above.

Taking as an example, where $P\widehat{=}io_1;Q_1$ and $R\widehat{=}io_2;Q_2$, then the $\textit{ok}$ signal of P can be computed by $\textit{ok}_P = f(\textit{ok} \wedge \textit{re}_P \wedge (\lnot \textit{re}_R \vee (Ran<0)))$. This means that when the external choice starts ($\textit{ok} = 1$) and the matching event of $io_1$ is ready ($\textit{re}_P = 1$), P is chosen to execute if either the matching event of $io_2$ is not ready ($\textit{re}_R = 0$), or the random number $\textit{Ran}$, where $\textit{Ran} \in [-1,1)$, occurs to be negative ($\textit{Ran} < 0$) when both of the matching event are ready. A keep pattern f(s) is used here to keep the signal $\textit{ok}_P$ true, otherwise it may jump back to false after that the communication terminates. The subsystem R is handled analogously. Thus, the output signals of the subsystem of are given by $\textit{ok}' = \textit{ok}'_P \vee \textit{ok}'_R$, $x' = \left\{ \begin{array}{lll} x'_P, &{} \textit{ok}'_P \\ x'_R, &{} \textit{ok}'_R \\ x, &{} \lnot \textit{ok}'_P \wedge \lnot \textit{ok}'_R \end{array} \right. .$

3.13 Interruption

Obviously, is equivalent to , where $\textit{re}'_R = f \left( \bigvee \nolimits _{i \in I} \textit{re}'_{oi_i} \right)$, and the translation rules can be composed in a semantic-preserving way (see Sect. 4). Hence, translating an interruption into a Simulink diagram becomes a composition of translating various components that have been illustrated in previous subsections.

4 Correctness of the Translation

In this section, we define UTP semantics both for HCSP constructs and the corresponding Simulink diagrams; proving the consistency of the two semantics is then a justification of the correctness of the translation from HCSP processes to Simulink diagrams.

UTP is a relational calculus based on first-order logic, which is intended for unifying different programming paradigms. In UTP, a sequential program (possibly nondeterministic) is represented by a design $D=(\alpha , P)$, where $\alpha$ denotes the set of state variables (called observables). Each state variable comes in an unprimed and a primed version, denoting respectively the pre- and the post-state value of the execution of the program. In addition to the program variables and their primed versions such as $x$ and $x'$, the set of observables includes two designated Boolean variables, $\textit{ok}$ and $\textit{ok}'$, denoting termination and stability of the program, respectively. $P$ stands for the construct, $p(x)\vdash R(x,x')$, which is defined as

$$\begin{aligned} (\textit{ok}{\wedge }p(x))\Rightarrow (\textit{ok}'\!{\wedge }R(x,x')). \end{aligned}$$

It means that if the program is activated in a stable state, $\textit{ok}$, where the precondition $p(x)$ holds, the execution will terminate, $\textit{ok}'$, in a state where the postcondition $R$ holds; thus the post-state $x'$ and the initial state $x$ are related by relation $R$. We use $\textit{pre}.D$ and $\textit{post}.D$ to denote the pre- and post-conditions of $D$, respectively. If $p(x)$ is $\textit{true}$, then $P$ is shortened as $\vdash R(x,x')$.

Refinement

Let $D_1 = (\alpha ,P_1)$ and $D_2= (\alpha ,P_2)$ be two designs with the same alphabet. $D_2$ is a refinement of $D_1$, denoted by $D_1\sqsubseteq D_2$, if $\forall x,x',\textit{ok},\textit{ok}' . \ (P_2\Rightarrow P_1)$. Aslo, let $D_1 = (\alpha _1,P_1)$ and $D_2= (\alpha _2,P_2)$ be two designs with possible different alphabets $\alpha _1=\{x,x'\}$ and $\alpha _2=\{y,y'\}$. $D_2$ is a data refinement of $D_1$ over $\alpha _1 \times \alpha _2$, denoted by $D_1\sqsubseteq _d D_2$, if there is a relation $\rho (y,x')$ s.t. $\rho (y, x'); D_1 \sqsubseteq D_2;\rho (y,x')$.

In UTP the domain of designs forms a complete lattice with the refinement partial order, and $\textit{true}$ corresponding to abort ($\textit{false}$ corresponding to miracle) is the smallest (largest) element of the lattice. Furthermore, this lattice is closed under the classical programming constructs. These fundamental mathematical properties ensure that the domain of designs is a proper semantic domain for sequential programming languages.

Concurrent and Reactive Designs

Semantics of concurrent and reactive programs is defined by the notion of reactive designs with an additional Boolean observable $\textit{wait}$ that denotes suspension of a program. A design $P$ is a reactive design if it is a fixed point of $\mathcal {H}'$, i.e. $\mathcal {H}'(P)=P$, where

$$\begin{aligned} \mathcal{H}'(p\vdash R) \widehat{=}( \vdash \wedge _{x\in \alpha (P)}\,x'=x \wedge \textit{wait}' = \textit{wait} ) \lhd \textit{wait}~\rhd (p \vdash R ). \end{aligned}$$

(1)

$P_1 \lhd b \rhd P_2$ is a conditional statement, which means if $b$ holds then $P_1$ else $P_2$, where $b$ is a Boolean expression and $P_1$ and $P_2$ are designs. Informally, Eq. (1) says that if a reactive system (a reactive design) waits for a response from the environment (i.e., $\textit{wait}$ holds), it will keep waiting and do nothing (i.e., keep program variables unchanged), otherwise its function ($p \vdash R$) will be executed.

Adaptation to Dynamical Systems

Obviously, hybrid systems are concurrent and reactive systems, so the UTP semantics of a hybrid system should satisfy the UTP healthiness condition. On the other hand, hybrid systems show some additional features, like real-time and the mixture of discrete and continuous dynamics. For specifying these additional features, we have to extend the notion of reactive design in UTP to admit function variables, and quantifications over functions, as in a real-time setting, program variables and channels are interpreted as functions over time. For specifying locality, higher-order quantifications are inevitable. So, UTP will become higher-order, rather than first-order. In addition, the derivative of a variable is allowed in a predicate. Therefore, strictly speaking, we extend the relational calculus of UTP to the combined theory of ordinary differential equations and timed traces with higher-order quantification.

In order to deal with real-time, a system variable $\textit{now}$ is introduced, which stands for the starting time. Correspondingly, $\textit{now}'$ stands for the ending time of a process.

Another point is that synchronization can only block discrete dynamics and keep discrete variable unchanged, it cannot block the evolution of continuous dynamics; time does not stop. So, given a hybrid system S, say $p\vdash P$, with continuous variables $\mathbf {s}$ and discrete variables $\mathbf {x}$, whose continuous dynamics is modeled as $\langle F(\dot{\mathbf {s}},\mathbf {s})=0 \& B \rangle$, written $S_C$ ², then the healthiness condition of reactive designs should be changed to

$$\begin{aligned}&\mathcal {H}(S) = S, \text{ where } \end{aligned}$$

(2)

$$\begin{aligned}&\mathcal {H}(S) \widehat{=}(\vdash \mathbf {x}'=\mathbf {x}\wedge \textit{wait}'=\textit{wait} \wedge S_C ) \, \lhd \textit{wait} \rhd \, S. \end{aligned}$$

(3)

A design that meets the healthiness condition (2) is called a hybrid design. For simplicity, we will denote the left side of $\textit{wait}$ in Eq. (3) by $\varPi _H$ in the sequel.

For convenience, for each channel $\textit{ch}$, we introduce two Boolean functions over time $\textit{ch}!$ and $\textit{ch}?$. $\textit{ch}!(t)$ means that $\textit{ch}$ is ready for sending at time t, similarly, $\textit{ch}?(t)$ means that $\textit{ch}$ is ready for receiving at time t. In addition, ${\text {Periodic}({ \textit{ch*}},{ \textit{st}})}$ denotes , which means that the communication event $\textit{ch*}$ is ready periodically with period $\textit{st}$. Also, maximal synchronization semantics is adopted, i.e.,

$$\begin{aligned} \forall t\ge 0.\ (\textit{ch}?(t) \wedge \textit{ch}!(t)) \Rightarrow (\lnot \textit{ch}?'(t) \wedge \lnot \textit{ch}!'(t)), \end{aligned}$$

(4)

which means that when a synchronization is ready, it takes place immediately.

4.1 UTP Semantics for Simulink

For each Simulink construct C, the observables of C include the inputs $\textit{in}$, outputs $\textit{out}$, the user defined parameters, and some auxiliary variables that are introduced for defining the semantics. Some output(s) may be also input(s), i.e. $\textit{out}_i=\textit{in}_j'$, but we will uniformly use $\textit{out}_i$ instead of $\textit{in}_j'$ as output in the semantics. Also, we use $\textit{cnow}$ to denote the current time. Now the semantics is a predicate denoted by $[\![C ]\!]$.

Blocks. As pointed out in [38], it is natural to interpret each block of a Simulink diagram as a predicate relating its inputs to the outputs. The behavior of a block can be divided into a set of sub-behaviors, each guarded by a condition. Moreover, these guards are exclusive and complete, i.e., the conjunction of any two of them is unsatisfiable and the disjunction of all of them is valid. So, each sub-behavior can be further specified as a predicate over input and output signals. Additionally, for each discrete block (diagram), it is assumed that its input signals from outside are available at each sampling point. So, it can be represented by a UTP formula of the form:

$$\begin{aligned}&\quad [\![B(\textit{ps},\textit{in}, \textit{out}) ]\!] \nonumber \\&\widehat{=}\mathcal {H}(\textit{Ass} \vdash \textit{out}(0)=\textit{ps}.\textit{init} \wedge \bigwedge _{k=1}^{m} (B_k(\textit{ps},\textit{in})\Rightarrow P_k(\textit{ps},\textit{in},\textit{out}))), \end{aligned}$$

(5)

which means that in case the environment satisfies Ass (the precondition), the behaviour of a block is specified by the formula at the right side of $\vdash$ (the postcondition). We use $\textit{ps}$ to denote a family of user-set parameters that may change the functionality of the block. As explained previously, $\bigvee _{k=1}^{m} B_k(\textit{ps},\textit{in})$, and $\lnot (B_i(\textit{ps},\textit{in}) \wedge B_j(\textit{ps},\textit{in}))$ for any $i\ne j$, always hold.

Thus the UTP semantics of a continuous block has the following form:

where $F_i(\dot{\textit{out}},\textit{out},\textit{in},\textit{ps})=0$ models the continuous evolution if $B_i$ holds. In this case, $\textit{wait} \, \widehat{=}\, \lnot \textit{out}?$ , which means that the continuous evolution will be interrupted by outputting to the environment. Thus, Eq. (2) holds with the maximal synchronization assumption in Eq. (4).

Correspondingly, the UTP semantics of a discrete block is

where $[\![P_{\textit{comp}_i}(\textit{in},\textit{out},\textit{ps}) ]\!]$ stands for the UTP semantics of the i-th discrete computation, which can be obtained in a standard way (see [37]). The precondition says that the environment should periodically input to and output from the block. In this case, $\textit{wait}$ is set as and its continuous is $\dot{\textit{cnow}}=1$, meaning that the block keeps waiting (idle) except for the periodic points at which discrete jumps happen.

Example 1

As an illustration, we show how to concretize the UTP semantics for some basic Simulink blocks including $\mathtt{\small Constant}$, $\mathtt{\small Divide}$, $\mathtt{\small Not}$, $\mathtt{\small Or}$, $\mathtt{\small Relational}$, $\mathtt{\small Switch}$, $\mathtt{\small Delay}$ and $\mathtt{\small Integrator}$. We treat $\mathtt{\small Constant}$ and $\mathtt{\small Delay}$ as continuous blocks, although they can also be treated as discrete blocks in a similar way.

A $\mathtt{\small Constant}$ block generates a scalar constant value:

$$\begin{aligned}{}[\![\mathtt{\small Constant}(\textit{ps.c}, \textit{out}) ]\!] ~ \widehat{=}~ \mathcal {H} ( \vdash \, \textit{out}(0) = c \wedge \dot{\textit{out}} =0\wedge \textit{out}!). \end{aligned}$$

The design inside $\mathcal {H}$ is equivalent to $\vdash \, \textit{out} =c \wedge \textit{out}!$, which is $\vdash \, \textit{out}(\textit{cnow}) =c \wedge \textit{out}!(\textit{cnow})$. Analogous remarks apply for the following.

Similarly, the UTP semantics for the $\mathtt{\small Divide}$ block is as follows:

The logical operator blocks $\mathtt{\small Not}$ and $\mathtt{\small Or}$ respectively perform the specified logical operations on their inputs, whose UTP semantics are given by

The $\mathtt{\small Relational}$ operator block compares two inputs using the relational operator parameter $\textit{ps}.\textit{op}$, and outputs either 1 (true) or 0 (false); its UTP semantics is given by

The $\mathtt{\small Switch}$ block passes through the first input or the third input based on the value of the second input, thus its UTP semantics is:

A $\mathtt{\small Delay}$ block holds and delays its input by one sample period, therefore its UTP semantics is:

$$\begin{aligned}&[\![ \mathtt{\small Delay}(\textit{ps}, \textit{in}, \textit{out}) ]\!] \widehat{=}\mathcal {H} ( \textit{in}!\vdash \left( \begin{array}{l} \textit{cnow} < ps.\textit{st} \Rightarrow \textit{out}(\textit{cnow}) = ps.\textit{init} \wedge \\ \textit{cnow} \ge ps.\textit{st} \Rightarrow \textit{out}(\textit{cnow}) = \textit{in}(\textit{cnow}-ps.\textit{st}) \end{array}\right) \wedge \textit{out}! ). \end{aligned}$$

An $\mathtt{\small Integrator}$ block outputs the value of the integral of its input signal with respect to time, so its UTP semantics is given by

Diagrams. A diagram is a set of blocks with connecting wires. W.l.o.g., consider a diagram D consisting of m continuous blocks and n discrete blocks, which are connected via a set of wires. The UTP semantics for blocks were defined above. Let therefore the semantics for the continuous blocks be $[\![C\!B_i( \textit{ps}_i, \{\textit{in}_i\}_{i\in I_i}, \textit{out}_i) ]\!]$ for $i=1,\ldots , m$, and for the discrete blocks be $[\![D\!B_j( \textit{ps}_j',\{\textit{in}_i'\}_{j\in J_j}, \textit{out}_j') ]\!]$ for $j=1,\ldots , n$.

Then the UTP semantics of D can be represented by

where $\mathrm {GCD}$ computes the greatest common divisor, and

$$\begin{aligned} \{\textit{in}_i^*\}_{i\in I_C}= & {} \cup _{i=1}^m \{\textit{in}_i\}_{i\in I_i} - (\{\textit{out}_1,\ldots \textit{out}_m\} \cup \{\textit{out}_1',\ldots , \textit{out}_n'\} ), \\ \{\textit{in}_i^*\}_{i\in I_D}= & {} \cup _{j=1}^n \{\textit{in}_j'\}_{j\in J_j} - (\{\textit{out}_1,\ldots \textit{out}_m\} \cup \{\textit{out}_1',\ldots , \textit{out}_n'\} ), \\ \{\textit{out}_i^*\}_{i\in J_C}= & {} \{\textit{out}_1,\ldots \textit{out}_m\} - (\cup _{i=1}^m \{\textit{in}_i\}_{i\in I_i} \cup \cup _{j=1}^n \{\textit{in}_j'\}_{j\in J_j}), \\ \{\textit{out}_i^*\}_{i\in J_D}= & {} \{\textit{out}_1',\ldots , \textit{out}_n'\} -(\cup _{i=1}^m \{\textit{in}_i\}_{i\in I_i} \cup \cup _{j=1}^n \{\textit{in}_j'\}_{j\in J_j}); \end{aligned}$$

$I_C$ and $I_D$ stand for the dangling inputs for continuous and discrete blocks after the composition, thus $I = I_C \cup I_D$ is the set of inputs of D; $J_C$ and $J_D$ stand for the dangling outputs for continuous and discrete blocks after the composition, thus $J = J_C \cup J_D$ is the set of outputs of D; and $\sigma$ and $\rho$ stand for the substitutions that replace the local input signals and input channels by the corresponding output signals and channels with the common names among these blocks (continuous and discrete) in each block, respectively. Furthermore, we set in this case

Example 2

Consider the diagram $\mathtt{\small Diag}$ performing $\textit{out} = \textit{in} + c$ . According to the above discussion, its UTP semantics can be given as

$$\begin{aligned}&\quad [\![ \mathtt{\small Diag}(\textit{ps}, \textit{in}, \textit{out}) ]\!] \\&\widehat{=}\exists \textit{out}'. \mathcal {H}( {\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{st}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{st}})} \vdash ( [\![ \mathtt{\small Constant}(\textit{ps}, \textit{out}'] ]\!] \wedge \\&\qquad \quad \qquad \quad \qquad \qquad [\![\mathtt{\small Add}(\textit{ps}, \{+1,+1\}, \{\textit{in}_1,\textit{in}_2\}, \textit{out}) ]\!][\textit{in}/\textit{in}_1, \textit{out}'/\textit{in}_2]). \end{aligned}$$

Subsystems

Normal Subsystems. A normal subsystem has a set of blocks and wires that specify the signal connections. Actually, a normal subsystem can be seen as a diagram by flattening, i.e., connecting the external inputs of the inside blocks with the inputs of the subsystem and the external outputs of the inside blocks with the outputs of the subsystem. Suppose a normal subsystem $\mathtt{\small NSub}$ with a set of inputs $\{\textit{in}_i\}_{i\in I}$ and a set of outputs $\{\textit{out}_j\}_{j\in J}$, and its inside blocks form a diagram $\mathtt{\small Diag}$ with a set of external inputs $\{\textit{in}_i'\}_{i\in I'}$ and $\{\textit{out}_j'\}_{j\in J'}$. Let $\sigma$ be the mapping to relate $\{\textit{in}_i\}_{i\in I}$ with $\{\textit{in}_i'\}_{i\in I'}$, and $\{\textit{out}_j'\}_{j\in J'}$ with $\{\textit{out}_j\}_{j\in J}$, then the UTP semantics of it can be easily defined as

$$\begin{aligned}{}[\![ \mathtt{\small NSub}(ps, \{\textit{in}_i\}_{i\in I}, \{\textit{out}_j\}_{j\in J} ]\!] ~\widehat{=}~ [\![ \mathtt{\small Diag}(ps, \{\textit{in}_i'\}_{i\in I'}, \{\textit{out}_j'\}_{j\in J'} ]\!][\sigma ]. \end{aligned}$$

Enabled Subsystems. A normal subsystem is enabled by adding an enabled block. It executes each simulation step when the enabling signal has a positive value, otherwise holds the states so they keep their most recent values. So, its UTP semantics can be defined as follows:

$$\begin{aligned}&[\![ \mathtt{\small ESub}( ps, \{\textit{in}_i\}_{i \in I}, en, \{\textit{out}_j\}_{j\in J}) ]\!] \\ \widehat{=}~~&\ en(now) > 0 \Rightarrow [\![ \mathtt{\small NSub}(ps, \{\textit{in}_i\}_{i \in I}, en, \{\textit{out}_j\}_{j\in J}) ]\!] \wedge \\ ~~&\ en(now) \le 0 \Rightarrow \textit{out}(now) = \textit{out}(now -ps.\textit{st}). \end{aligned}$$

Theorem 1

Given a Simulink diagram C, its UTP semantics $[\![C ]\!]$ satisfies the healthiness condition in Eq. (2), that is

$$\begin{aligned} \mathcal {H}([\![C ]\!] )=[\![C ]\!]. \end{aligned}$$

Proof

It is straightforward by the definition of $[\![C ]\!]$.    $\square$

4.2 UTP Semantics for HCSP

As advocated by Hoare and He [37], a reactive system can be identified by the set of all possible observations of that system. As usual, an alphabet is attached to a system P (and its with the following constituents: $\mathcal {V}(P)$: the set of both continuous and discrete variable names, which is arranged as a vector $\mathbf {v}$, $i\varSigma (P)$: the set of input channel names, and $o\varSigma (P)$: the set of output channel names. Together the latter two form $\varSigma (P) \widehat{=}i\varSigma (P) \cup o\varSigma (P)$, which is arranged as a vector $\textit{ch}_P$.

Given a hybrid system, its timed observation is the tuple $\langle \textit{now}, \mathbf {v}, \mathbf {f}_{\mathbf {v}}, \textit{re}_{\textit{ch}*}, \textit{msg}_{\textit{ch}} \rangle$. Here $\textit{now}$ is the start point and $\textit{now}'$ the end point of a time interval of an observation i. The initial values of variables are $\mathbf {v}$, and $\mathbf {v}'$ are the final values at termination. The vector $\mathbf {f}_{\mathbf {v}}$ contains of real-valued functions over the time interval $[\textit{now}, \textit{now}']$ that record the values of $\mathbf {v}$, evidently with $\mathbf {f}_{\mathbf {v}}(\textit{now}) = \mathbf {v}, \mathbf {f}_{\mathbf {v}}(\textit{now}') = \mathbf {v}'$. The vector $\textit{re}_{\textit{ch}*}$ of $\{0, 1\}$-valued Boolean functions over $[\textit{now}, \textit{now}']$, indicates whether communication events $\textit{ch}*$ are ready for communication. The vector $\textit{msg}_{\textit{ch}}$, of real-valued functions over $[\textit{now}, \textit{now}']$ records the values passed along channels $\textit{ch}$. We further define

$$\begin{aligned} \textit{const}(\mathbf {f},\mathbf {b}, t_1,t_2)&\widehat{=}\forall t \in [t_1,t_2]. \ \mathbf {f}(t) = \mathbf {b},\\ \textit{const}^l(\mathbf {f},\mathbf {b},t_1,t_2)&\widehat{=}\forall t \in [t_1,t_2). \ \mathbf {f}(t) = \mathbf {b},\\ \textit{const}^r(\mathbf {f},\mathbf {b},t_1,t_2)&\widehat{=}\forall t \in (t_1,t_2]. \ \mathbf {f}(t) = \mathbf {b}. \end{aligned}$$

Using the UTP timed observations, the HCSP constructs can be defined as follows.

The $\text {skip}$ statement, which does not alter the program state, is the relational identity:

$$\begin{aligned}&[\![ \text {skip} ]\!] \widehat{=}\mathcal {H} (\vdash \textit{now}'=\textit{now} \wedge \mathbf {v}' = \mathbf {v}\wedge \textit{const}(\mathbf {f}_\mathbf {v},\mathbf {v},\textit{now},\textit{now}') \wedge \\&\qquad \qquad \textit{const}(\textit{re}_{\textit{ch}*},\mathbf 0 ,\textit{now},\textit{now}') \wedge \textit{const}(\textit{msg}_{\textit{ch}}, \textit{msg}_{\textit{ch}}(\textit{now}),\textit{now},\textit{now}')). \end{aligned}$$

As $\text {skip}$ terminates immediately, $\textit{wait}$ is equivalent to $\textit{false}$ in this case. Hereafter, let

$$\begin{aligned} \textit{RE} ~\widehat{=}~ \textit{const}(\textit{re}_{\textit{ch}*},\mathbf 0 ,\textit{now},\textit{now}') \wedge \textit{const}(\textit{msg}_{\textit{ch}},\textit{msg}_{\textit{ch}}(\textit{now}),\textit{now},\textit{now}'). \end{aligned}$$

The assignment of e to a variable x is modelled as setting x to e and keeping all other variables (denoted by $\mathbf {u}$) constant:

$$\begin{aligned}&[\![ x:=e ]\!] \widehat{=}\mathcal {H} (\vdash \textit{now}'=\textit{now} \wedge x' = e \wedge \mathbf {u}' = \mathbf {u}\wedge \textit{const}(\mathbf {f}_x,e,\textit{now},\textit{now}') \wedge \\&\qquad \quad \qquad \textit{const}(\mathbf {f}_{\mathbf {u}},\mathbf {u},\textit{now},\textit{now}') \wedge \textit{RE}). \end{aligned}$$

As an assignment process terminates immediately, $\textit{wait}$ is equivalent to $\textit{false}$ here.

An evolution process says that the system waits, while it is evolving until the domain constraint becomes false. So, the UTP semantics is the following hybrid design

$$ \begin{aligned}{}[\![ \langle {F}(\dot{s},s)=0 \& B\rangle ]\!] ~\widehat{=}~ (\vdash F(\dot{s},s=0)\wedge \dot{t}=1 ) \lhd B \rhd [\![\text {skip} ]\!]. \end{aligned}$$

Obviously, in this case $\textit{wait}$ is equivalent to B.

The conditional statement behaves according to whether the condition holds or not: $[\![ B \rightarrow P ]\!] ~ \widehat{=}~[\![P ]\!] \lhd B \rhd [\![\text {skip} ]\!]$, and internal choice is interpreted as a non-deterministic selection between two operands: $[\![ P \sqcup Q ]\!] ~ \widehat{=}~ ([\![ P ]\!] \vee [\![ Q ]\!]).$

In order to define sequential and parallel composition, we introduce two semantic operators.

Let $H_1$ and $H_2$ be two hybrid designs with

$$\begin{aligned}&H_1 \widehat{=}(\vdash \wedge _{x\in \mathcal {V}(H_1)}\,x'=x \wedge \textit{wait}_{H_1}' = \textit{wait}_{H_1} \wedge S_{H_1}) \lhd \textit{wait}_{H_1} \rhd (p_{H_1} \vdash R_{H_1}), \\&H_2 \widehat{=}(\vdash \wedge _{x\in \mathcal {V}(H_2)}\,x'=x \wedge \textit{wait}_{H_2}' = \textit{wait}_{H_2} \wedge S_{H_2}) \lhd \textit{wait}_{H_2} \rhd (p_{H_2} \vdash R_{H_2}), \end{aligned}$$

which satisfy the healthiness condition in Eq. (2). The sequential composition of $H_1$ and $H_2$, denoted by is defined by

where

$$\begin{aligned} \sigma _{H_1}= & {} [\mathbf {v}_{H_1}/\mathbf {v}',\textit{now}_{H_1}/\textit{now}',\textit{ok}_{H_1}/\textit{ok}'][\mathbf {f}_{\mathbf {v}_{H_1}}/\mathbf {f}_{\mathbf {v}},\textit{re}_{\textit{ch}_{H_1}\!\!*}/ \textit{re}_{\textit{ch}*},\textit{msg}_{\textit{ch}_{H_1}}/\textit{msg}_{\textit{ch}}], \\ \sigma _{H_2}= & {} [\mathbf {v}_{H_1}/\mathbf {v},\textit{now}_{H_1}/\textit{now},\textit{ok}_{H_1}/\textit{ok}][\mathbf {f}_{\mathbf {v}_{H_2}}/\mathbf {f}_{\mathbf {v}}, \textit{re}_{\textit{ch}_{H_2}\!\!*}/\textit{re}_{\textit{ch}*}, \textit{msg}_{\textit{ch}_{H_2}}/\textit{msg}_{\textit{ch}}]. \end{aligned}$$

In the above,

$$\begin{aligned}& \exists \mathbf {v}_{H_1},\textit{now}_{H_1},\textit{ok}_{H_1}. \ \exists \mathbf {f}^{H_1}_{\mathbf {v}},\textit{re}_{\textit{ch}_{H_1}\!\!*},\textit{msg}_{\textit{ch}_{H_1}},f^{H_2}_{\mathbf {v}},\textit{re}_{\textit{ch}_{H_2}\!\!*},\textit{msg}_{\textit{ch}_{H_2}}. \ \\&\quad (\lnot \textit{wait}_{H_1} \wedge \textit{wait}_{H_2} \wedge r_{H_1} \vdash R_{H_1})\sigma _{H_1} \wedge (\lnot \textit{wait}_{H_1} \wedge \lnot \textit{wait}_{H_2} \wedge r_{H_2} \vdash R_{H_2})\sigma _{H_2} \end{aligned}$$

is essentially equivalent to the sequential composition of the two designs $(\lnot \textit{wait}_{H_1} \wedge \textit{wait}_{H_2} \wedge r_{H_1} \vdash R_{H_1})$ and $(\lnot \textit{wait}_{H_1} \wedge \lnot \textit{wait}_{H_2} \wedge r_{H_2} \vdash R_{H_2})$ by the theory of UTP [37].

It is easy to see that if $H_1$ and $H_2$ satisfy the healthiness condition of hybrid designs, so does . Hence, is still a hybrid design, which implies that hybrid designs are closed under sequential composition.

The parallel composition of $H_1$ and $H_2$, denoted by $H_1 \parallel H_2$ is defined

$$\begin{aligned} H_1 \Vert H_2 ~\widehat{=}&\exists \textit{now}_{H_1},\textit{now}_{H_2},\textit{ok}_{H_1},\textit{ok}_{H_2}. \ H_1[\textit{ok}/\textit{ok}_{H_1}] \wedge H_2[\textit{ok}/\textit{ok}_{H_2}] \wedge \\&\textit{now}'=max\{\textit{now}'_{H_1},\textit{now}'_{H_2}\} \wedge (\textit{ok}' = \textit{ok}'_{H_1} \wedge \textit{ok}'_{H_2}) \wedge \\&(\forall t \in (\textit{now}'_{H_1},\textit{now}']. \ \mathbf {f}_{\mathbf {v}_{H_1}}(t)=\mathbf {f}_{\mathbf {v}_{H_1}}(\textit{now}'_{H_1}) \wedge \\&~~ \ \textit{re}_{\textit{ch}_{H_1}\!\!*}(t)=\textit{re}_{\textit{ch}_{H_1}\!\!*}(\textit{now}'_{H_1}) \wedge \textit{msg}_{\textit{ch}_{H_2}}(t) = \textit{msg}_{\textit{ch}_{H_2}}(\textit{now}'_{H_2})) \wedge \\&(\forall t \in (\textit{now}'_{H_2},\textit{now}']. \ \mathbf {f}_{\mathbf {v}_{H_2}}(t)=\mathbf {f}_{\mathbf {v}_{H_2}}(\textit{now}'_{H_2}) \wedge \\&~~ \ \textit{re}_{\textit{ch}_{H_2}\!\!*}(t)=\textit{re}_{\textit{ch}_{H_2}\!\!*}(\textit{now}'_{H_2}) \wedge \textit{msg}_{\textit{ch}_{H_2}\!\!*}(t) = \textit{msg}_{\textit{ch}_{H_2}\!\!*}(\textit{now}'_{H_2})). \end{aligned}$$

It can be further be proved that

$$\begin{aligned} H_1 \Vert H_2 ~&\Leftrightarrow ~ \exists \textit{now}_{H_1},\textit{now}_{H_2},\textit{ok}_{H_1},\textit{ok}_{H_2}. \\&\vdash \left( \begin{array}{l} \textit{wait}_{H_1} \Rightarrow \varPi _{H_1} \wedge \\ \textit{wait}_{H_2} \Rightarrow \varPi _{H_2} \end{array} \right) \lhd \textit{wait}_{H_1}\wedge \textit{wait}_{H_2} \rhd \left( \begin{array}{l} (p_{H_1} \vdash R_{H_1})[\textit{ok}/\textit{ok}_{H_1}] \wedge \\ (p_{H_2} \vdash R_{H_2})[\textit{ok}/\textit{ok}_{H_2}] \end{array} \right) \wedge \\& \textit{now}'=max\{\textit{now}'_{H_1},\textit{now}'_{H_2}\} \wedge (\textit{ok}' = \textit{ok}'_{H_1} \wedge \textit{ok}'_{H_2}) \wedge \\&(\forall t \in (\textit{now}'_{H_1},\textit{now}']. \ \mathbf {f}_{\mathbf {v}_{H_1}}(t)=\mathbf {f}_{\mathbf {v}_{H_1}}(\textit{now}'_{H_1}) \wedge \\&~~ \ \textit{re}_{\textit{ch}_{H_1}\!\!*}(t)=\textit{re}_{\textit{ch}_{H_1}\!\!*}(\textit{now}'_{H_1}) \wedge \textit{msg}_{\textit{ch}_{H_2}}(t) = \textit{msg}_{\textit{ch}_{H_2}}(\textit{now}'_{H_2})) \wedge \\&(\forall t \in (\textit{now}'_{H_2},\textit{now}']. \ \mathbf {f}_{\mathbf {v}_{H_2}}(t)=\mathbf {f}_{\mathbf {v}_{H_2}}(\textit{now}'_{H_2}) \wedge \\& ~~ \ \textit{re}_{\textit{ch}_{H_2}\!\!*}(t)=\textit{re}_{\textit{ch}_{H_2}\!\!*}(\textit{now}'_{H_2}) \wedge \textit{msg}_{\textit{ch}_{H_2}\!\!*}(t) = \textit{msg}_{\textit{ch}_{H_2}\!\!*}(\textit{now}'_{H_2})). \end{aligned}$$

Therefore,also $H_1\parallel H_2$ satisfies the healthiness condition of hybrid designs. Hence, $H_1\parallel H_2$ is a hybrid design, which implies that hybrid designs are closed under parallel composition.

Now, given two HCSP processes P and Q, their sequential composition is defined , and their parallel composition by $[\![P\parallel Q ]\!] ~ \widehat{=}~ [\![P ]\!] \parallel [\![Q ]\!]$.

A process variable X is interpreted as a predicate variable. Without confusion in the context, we use X to represent the predicate variable corresponding to process variable X, i.e. $[\![X ]\!] ~~ \widehat{=}~~ X$.

The semantics for recursion is defined as the least fixed point of the corresponding recursive predicate by $[\![ \mathrm {rec}\, X. P ]\!] ~~ \widehat{=}~~ \mu X. [\![ P ]\!]$. An HCSP process $P^*$ is thus defined as $P^* \, \Leftrightarrow \, \mathrm {rec}\, X. (\text {skip}\, \sqcup \, (P \, ; \, X))$. As discussed above, its semantics is given by $[\![P^* ]\!] \, \, \Leftrightarrow \, \exists N. [\![P^N ]\!]$, where $P^0 \, \widehat{=}\, \text {skip}$.

A receiving event can be modelled by $[\![\textit{ch}?x ]\!] ~\widehat{=}~ \vdash \textit{LHS} \lhd \textit{re}_{\textit{ch}?} \wedge \lnot \textit{re}_{\textit{ch}!} \rhd \textit{RHS}$, where $\textit{LHS} \widehat{=}\dot{now}=1\wedge x'=x \wedge \mathbf {u}'=\mathbf {u}$, and

$$\begin{aligned}&\textit{RHS} \widehat{=}\textit{now}'=\textit{now}+d \wedge \textit{re}_{\textit{ch}?}'=0 \wedge \textit{re}_{\textit{ch}!}'=0 \wedge \mathbf {u}'=\mathbf {u}\wedge x'=\textit{msg}_{\textit{ch}}(\textit{now}') \wedge \\&\qquad \quad \textit{const}^l(\textit{re}_{\textit{ch}?},1,\textit{now},\textit{now}') \wedge \textit{const}^l(\textit{re}_{\textit{ch}!},0,\textit{now},\textit{now}'). \end{aligned}$$

Here, $\textit{wait} \ \widehat{=}\ \textit{re}_{\textit{ch}?} \wedge \lnot \textit{re}_{\textit{ch}!}$, i.e., the process waits until its dual event becomes ready. The sending event $[\![ \textit{ch}!e ]\!]$ can be defined similarly.

The communication interruption can be defined as

where $\varGamma \widehat{=}\bigvee \nolimits _{i \in I} \textit{re}'_{\overline{\textit{io}_i}}$, and $\overline{\textit{io}_i}$ stands for the dual communication event with respect to $\textit{io}_i$, for instance $\overline{\textit{ch}?}=\textit{ch}!$.

To prove whether the UTP semantics of other HCSP constructs satisfies the healthiness condition is mathematically straightforward and thus omitted here. It can be further deduced that the domain of hybrid designs forms a complete lattice with a refinement partial order, on which the classical programming operations are closed.

4.3 Justification of Correctness

Having defined a UTP semantics respectively for the HCSP components and the Simulink diagrams, we justify the translation by checking the semantic equivalence of a Simulink diagram with its corresponding HCSP construct (Theorem 2). Here are several remarks to be noted during the proofs:

• 1. We set the sample times of all discrete blocks to $-1$ in the translation, that is, all the generated discrete blocks share a globally identical sample time $\textit{gst}$, which will be configured by the user before triggering the simulation.

• 2. It is assumed that the $\textit{In}\_\textit{ok}$ signal in a subsystem firstly turns true at the first sample point, i.e. $\textit{min}\{t|\textit{In}\_\textit{ok}(t)=1\} = \textit{gst}$. Similarly, we use $\tau$ to denote the earliest time at which the $\textit{Out}\_\textit{ok}$ signal becomes true, i.e. $\tau \, \widehat{=}\, \textit{min}\{t|\textit{Out}\_\textit{ok}(t) = 1\}$.

• 3. Hereafter we use $[\![\mathtt{\small Wires} ]\!]$ to indicate implicitly the entire group of variable substitutions within a subsystem, and blocks are referred to as their abbreviated names with potential identifiers, for instance, $\mathtt{\small Swt1}$ in the assignment structure stands for the block $\mathtt{\small Switch1}$ in Fig. 3.

• 4. Unless otherwise stated, the parameters of a block will be elided in the semantic function for simplicity. Besides, to distinguish the input/output signals of blocks, the leading characters of input/output signals of a subsystem are capitalized.

Theorem 2

  Given an HCSP process P, denote the translated Simulink diagram by $\mathtt{\small H2S}(P)$. Suppose there is a correspondence (denoted by EA) between $[\![P ]\!]$ and $[\![\mathtt{\small H2S}(P) ]\!]$, i.e., $\textit{now} = \textit{gst}$, $\textit{now}' = \tau$, $\textit{ok} = \textit{In}\_\textit{ok}(\textit{gst}) =\top$, $\textit{ok}' = \textit{Out}\_\textit{ok}(\tau )$, $\mathbf {v}= \textit{In}\_{\mathbf {v}}(\textit{gst})$, $\mathbf {v}' = \textit{Out}\_{\mathbf {v}}(\tau )$, $f_{\mathbf {v}} = \textit{Out}\_{\mathbf {v}}|_{[\textit{gst}, \tau ]}$, $\textit{re}_{\textit{ch}*} = \textit{Out}\_\textit{re}_{\textit{ch}*}|_{[\textit{gst}, \tau ]}$, and $\textit{msg}_{\textit{ch}} = \textit{Out}\_\textit{re}_{\textit{ch}}|_{[\textit{gst}, \tau ]}$, then

$$\begin{aligned} {\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{gst}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{gst}})} \Rightarrow \left( [\![ P ]\!] \Leftrightarrow [\![\mathtt{\small H2S}(P) ]\!] |_{[\textit{gst}, \tau ]} \right) \end{aligned}$$

(6)

as $\textit{gst} \rightarrow 0$.

Proof

By induction on the structure of HCSP components. For simplicity, we use $\mathbf{ch }{*}$ to denote the local communication events inside of $\mathtt{\small H2S}(P)$ in what follows.  

$\text {skip}$::

It is easy to see that under the assumptions,

$$\begin{aligned} {\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{gst}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{gst}})} \Rightarrow \left( [\![ \text {skip} ]\!] \Leftrightarrow [\![ \mathtt{\small H2S}(\text {skip}) ]\!] |_{[\textit{gst}, \tau ]} \right) . \end{aligned}$$

Assignment: :

Without loss of generality, we use $[\![\mathtt{\small Diag}_e ]\!]$ to denote the semantics of the diagram which computes the right-hand side of the assignment.

Using the left-hand side of (6) and restricting the time interval, we get the desired result.

Evolution statement: :

By the defined UTP semantics, it follows

Using the left-hand side of (6) and restricting the time interval, we have

$$ \begin{aligned}&{\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{gst}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{gst}})} \wedge \textit{ok} \wedge [\![ \mathtt{\small H2S}(\langle {F}(\dot{s},s)=0 \& B\rangle ) ]\!] |_{[\textit{gst}, \tau -\textit{gst}}] \end{aligned}$$

Thereby the semantics can be proved consistent on the interval $[\textit{gst},\tau -\textit{gst}]$, moreover, when the user-defined sample time $\textit{gst} \rightarrow 0$, we have the desired result.

Conditional: :

By the definition of $\mathtt{\small H2S}$ and the UTP semantics of Simulink:

It follows

Thus we have the desired result.

Internal choice: :

This is proved as for the conditional process.

Sequential composition: :

As shown in Fig. 7, $\mathbf {x}$ are the set of common signals processed by both P and Q, while $\mathbf {y}$ and $\mathbf {z}$ are the respective exclusive signals.

This gives the desired result.

Recursion: :

We only consider tail recursion, i.e., repetition. General recursion can be proved similarly. As shown in Fig. 8, a random number N, generated by an oracle, is used in the Simulink diagram as the number of iterations of subsystem P. Since $[\![ P^* ]\!]$ is defined by the least fixed point, it is clear that the inverse direction holds: ${\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{gst}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{gst}})} \Rightarrow \left( [\![ P^* ]\!] \Leftarrow [\![ \mathtt{\small H2S}(P^*) ]\!] |_{[\textit{gst}, \tau ]} \right)$. For the other direction, suppose $[\![ P^* ]\!]$ holds, then according to the semantics, there must exist N such that $[\![ P^N ]\!]$ holds. We then apply the oracle, to generate the same number N, to control the execution of the Simulink diagram $\mathtt{\small H2S}(P^*)$, to execute for N times. The fact is thus proved, i.e.

$$\begin{aligned} {\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{gst}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{gst}})} \Rightarrow \left( [\![ P^* ]\!] \Rightarrow [\![ \mathtt{\small H2S}(P^*) ]\!] |_{[\textit{gst}, \tau ]} \right) . \end{aligned}$$

Communication events: :

By the definition of $\mathtt{\small H2S}$ and the UTP semantics of Simulink given in Sect. 4.1, it follows

Therefore, we get

$$\begin{aligned} {\text {Periodic}({ \textit{in}!},{ \textit{ps}.\textit{gst}})} \wedge {\text {Periodic}({ \textit{out}?},{ \textit{ps}.\textit{gst}})} \Rightarrow \left( [\![ \textit{ch}?x ]\!] \Leftrightarrow [\![ \mathtt{\small H2S}(\textit{ch}?x) ]\!] |_{[\textit{gst}, \tau ]} \right) . \end{aligned}$$

The equivalence for sending events can be proved similarly.

Interruption: :

It is trivial to prove that Theorem 2 holds for communication interruption, inasmuch as it can be interpreted by the sequential composition and conditional statement, for which we have already proved validation of Theorem 2.

Parallel: :

As shared variables are not allowed in HCSP, we use $\mathbf {y}$ and $\mathbf {z}$ to denote the set of exclusive signals (including $\textit{re}$ and $\textit{msg}$) respectively for P and Q. Let $\tau _\textit{P} \widehat{=}\textit{min}\{t|\textit{out}\_\textit{NSubP}\_\textit{ok}(t) = 1\}$, and $\tau _\textit{Q} \widehat{=}\textit{min}\{t|\textit{out}\_\textit{NSubQ}\_\textit{ok}(t) = 1\}$. Then, according to the definitions, we have

It thus follows immediately that Theorem 2 holds for the parallel composition.    $\square$

 

5 Conclusion

In this paper, we presented a translation from HCSP formal models into Simulink graphical models, so that the models can be simulated and tested using a MATLAB platform, thus avoiding expensive formal verification if the development is at a stage where it is considered unnecessary. Together with our previous work on encoding Simulink/Stateflow diagrams into HCSP, it provides a two-way path in the design of embedded systems. In addition, we proposed a justification of the translation, which uses UTP as a main vehicle for arguing formally for the correspondence between the two semantics.