# Proving Simulink Block Diagrams Correct via Refinement

Authors: Wei Zhang; Quan Sun; Chao Wang; Zhiming Liu
Journal: Wireless Communications and Mobile Computing
 (2022)

---

## Abstract

Simulink is a well-known block diagram-based tool for modular design and multidomain simulation of Cyber-Physical Systems (CPS). However, the simulation by Simulink cannot completely cover the state space or behavior of a target system, which would not ensure the correctness of the developed block diagrams in Simulink. In this work, we present a contract-based method, which supports compositional reasoning and refinement, for proving the correctness of Simulink block diagrams withdiscrete-time and continuous-time dynamic behavior. We use the assume-guarantee contract as a specification language. The Simulink block diagrams are correct in the sense that if the block diagrams satisfy the formal specifications of the system being modeled. To prove the correctness of a block diagram, we first define semantics for Simulink block diagrams. We study three composition operators, i.e., serial, parallel, and algebraic loop-free feedback with multistep delays. We present a satisfaction relation between the block diagram and contract and present a refinement relation between the contracts. We prove that if the Simulink block diagram satisfies the composition contract and the composition contract refines the system specifications, the block diagram is correct relative to the system specifications. Furthermore, we demonstrate the effectiveness of our method via a real-world case study originating from the control system of a reservoir. Our method can also provide an idea to verify whether the designed CPS is planted with a logic bomb by attackers.


---

## Body

## 1. Introduction

Cyber-Physical Systems (CPS) are engineering systems where functionalities emerge from the network interaction of physical and computational processes [1]. Designing CPS correctly and efficiently is a critical challenge for computer science and industry. Model-based design (MBD) [2] provides virtual system integration and a visual approach to develop models for CPS. Bugs in the model can be identified and corrected at an early stage of the design process when no hardware is available. Such a method is considered as an effective solution to design CPS correctly.Simulink [3] is a graphical modeling language for model-based design (MBD). Currently, Simulink greatly appeals to CPS engineers since it captures the dynamic behavior of the modeled system. A Simulink block diagram consists of blocks connected via wires. The blocks (from Simulink library, a set of predefined blocks that can assemble block diagrams of systems with drag-and-drop mouse operations) represent different parts of a system being modeled, and wires indicate the communication between the blocks. The blocks have input and output ports that receive the input signals and send the output signals. The signals are the functions of time that can be continuous-time or discrete-time. Hence, the Simulink block diagrams can be classified based on the time: contain only discrete-time blocks, continuous-time blocks, or a mixture of discrete-time and continuous-time blocks. Our work focuses on the Simulink block diagrams containing only discrete-time blocks and continuous-time blocks, which we call discrete-time Simulink block diagrams or continuous-time Simulink block diagrams.Simulink supports the design, modeling, simulation, and test of CPS. The test for Simulink block diagrams is based on numerical simulation. One of the drawbacks of numerical simulation is that it does not completely cover a target system’s state space or behavior. In addition, a logic bomb [4] maliciously inserted into Simulink by attackers can persistently change the behavior. In safety-critical systems, an error could lead to incorrect analysis results and thus result in property damage, even significant injury or death. Formal methods can rigorously prove that all possible behaviors satisfy a specific formal specification, thus ensuring correctness. By “correctness,” we mean that all possible behaviors of the Simulink block diagram satisfy the given formal specification of a system to be modeled.A number of methods have been reported in the literature. To the best of our knowledge, some existing solutions only focus on Simulink block diagrams withdiscrete-time behaviors, e.g. [5–11]. A common approach for tackling continuous-time Simulink block diagrams is to discretize the continuous-time dynamical behavior [12, 13]. However, the discretization of continuous systems reduces the accuracy of the verification of continuous dynamics. The contract supports compositional reasoning and refinement, enabling hierarchical design and verification of complex systems by decomposed system-level specification into the block-level specification to provide implementations correctly. Based on this advantage, we employ contract as formal specification to specify the observable trajectory of discrete-time and continuous-time blocks and present a contract-based refinement technique for proving Simulink block diagrams’ correctness.To prove the correctness of Simulink block diagrams, we first define formal semantics for Simulink block diagrams. We consider the blocks in the library to be units and call them elementary blocks. The elementary block expresses the time-dependent (continuous-time or discrete-time) relationships between the inputs, internal states, and outputs. Thus, we define the elementary block as a dynamic system that can model both continuous-time and discrete-time blocks. Based on this definition, we define the observable trajectory for the blocks, i.e., the evolution of the value of input-output variables over time. We formulate the wire as unilateral connection (i.e., the relations of output and input between connected blocks) for communication. Then, to construct the Simulink block diagrams, we define three basic composition operators, namely, serial, parallel, and algebraic loop-free feedback composition. Moreover, we study the algebraic loop-free feedback composition containing multistep delays. Similar works [13, 14] only considered the ones with unit delay.We then present a contract-based refinement technique to prove the correctness of the Simulink block diagrams, as shown in Figure1. Our purpose is to prove that the block diagram satisfies the system specification. To this end, we introduce a mid-level called composition contract (i.e., the composition of contracts corresponding to the blocks that construct the Simulink block diagrams) between low-level block diagrams and high-level system specifications for composition. The approach is divided into two stages. Firstly, we define the satisfaction relation that relates block to contract and verify that the satisfaction relation is preserved by composition, i.e., if blocks satisfy their contract, respectively, their composition satisfies the contract composition. Secondly, we define the refinement relation between contracts and prove that the composition of contracts refines the system specifications. The block diagram is correct as long as we prove that the block diagram satisfies the composition contract and the composition contract refines the system specification to imply that the block diagram satisfies the system specification.Figure 1
An overview of contract-based correctness proof methods for Simulink block diagrams, where the dashed line and⊨: satisfaction; ≼: refinement; ⊗: composition.


### 1.1. Contributions

Contributions of this paper are summarized as follows:(i)
We define the formal semantics for Simulink block diagrams from the viewpoint of dynamic systems to precisely express the trajectory of the Simulink block diagrams withdiscrete-time and continuous-time(ii)
Under the semantics, we propose a contract-based refinement technique mentioned above for proving the correctness of the Simulink block diagrams withdiscrete-time and continuous-time blocks(iii)
We demonstrate the effectiveness of our method through a case study of the control system of a reservoir that is modelled with Simulink block diagrams


### 1.2. Organization

The remainder of this paper is organized as follows. Section2 reviews the related works. Section 3 introduces the notations and notions used in our work. Section 4 presents the semantics of the Simulink block diagrams. Section 5 proposes the contract-based refinement method for proving the correctness of Simulink diagram blocks. Section 6 demonstrates the effectiveness of our method with a case study. Section 7 concludes the paper and proposes future works.


## 1.1. Contributions

Contributions of this paper are summarized as follows:(i)
We define the formal semantics for Simulink block diagrams from the viewpoint of dynamic systems to precisely express the trajectory of the Simulink block diagrams withdiscrete-time and continuous-time(ii)
Under the semantics, we propose a contract-based refinement technique mentioned above for proving the correctness of the Simulink block diagrams withdiscrete-time and continuous-time blocks(iii)
We demonstrate the effectiveness of our method through a case study of the control system of a reservoir that is modelled with Simulink block diagrams


## 1.2. Organization

The remainder of this paper is organized as follows. Section2 reviews the related works. Section 3 introduces the notations and notions used in our work. Section 4 presents the semantics of the Simulink block diagrams. Section 5 proposes the contract-based refinement method for proving the correctness of Simulink diagram blocks. Section 6 demonstrates the effectiveness of our method with a case study. Section 7 concludes the paper and proposes future works.


## 2. Related Works

In recent years, there are a range of methods to analyze and verify Simulink.There exist some works that translate Simulink into other formal modeling languages. For example, Tripakis et al. [5] translated the Simulink block diagrams to a synchronous dataflow language, Lustre. Since the Lustre has a discrete-time semantics, the work [5] only handled discrete-time Simulink block diagrams. In [6], Cavalcanti et al. presented a semantics for discrete-time Simulink blocks diagrams called Circus. The work [6] was based on existing tools that generate CSP and Z specifications from discrete-time block diagrams. It only translated discrete-time Simulink blocks diagrams, Simulink block diagrams with continuous-time were not considered.Chen and Dong [15, 16] presented the method to automatically transformed Simulink diagrams with discrete-time and continuous-time into Timed Interval Calculus (TIC) models. This method applied the Prototype Verification System (PVS) to validate that TIC fulfils requirements. These works were the first attempt to model Simulink block diagrams with continuous-time. The work [17] presented an operational semantics for Simulink’s simulation engine that formally defines the numerical simulation result, including discrete-time and continuous-time. Zou et al. [18] automatically translated Simulink block diagrams into Hybrid Communicating Sequential Processes (HCSP) and showed how the translated HCSP models are verified using the Hybrid Hoare Logic Verifier. In [19], it showed how different Simulink blocks can be expressed in the synchronous language Ze′lus, which extends a language Lustre with ODEs and zero-crossing events. The main difference between the articles [15–19] and our work is intentions. Our main goal here is not to translate the Simulink block diagrams to other formalisms, nor to define the semantics of Simulink’s engine, but to directly define the trajectory of the Simulink block diagrams from the point of view of dynamic systems and provide a compositional and refinement technology to prove the correctness of Simulink block diagrams with discrete-time and continuous-time. On the other hand, we have three basic composition operators, i.e., serial, parallel, and algebraic loop-free feedback composition with multistep delays, which more facilitate the composition in construction. However, the work [18] could verify hybrid system, which is not considered in our work.The contract-based approaches for verifying the correctness of Simulink block diagrams were also widely studied in the literature. Bostro et al. [7] showed definitions of contract and refinement using the action systems for Simulink models, while refinement provides a framework for reasoning about implementation correctness. However, this work only focuses on discrete-time Simulink block diagrams. Ye et al. [10, 11] defined a theoretical reasoning framework for Simulink block diagrams using Unifying Theories of Programming (UTP). The main idea of these papers is to translate each block or subsystem to a design, and the hierarchical connections of blocks are mapped to a variety of compositions of designs, and verify some properties. However, these papers only handled discrete-time Simulink block diagrams. In our work, we provide a compositional and refinement technology to prove the correctness of Simulink block diagrams with discrete-time and continuous-time. Dragomir et al. [13] recently presented a Refinement Calculus of Reactive Systems (RCRS) toolset for compositional formal modeling and reasoning about discrete and continuous reaction systems. RCRS is a discrete-time framework. The continuous systems can be modeled by discretizing time. However, the discretization of continuous systems reduces the accuracy of the verification of continuous dynamics. Our approach differs because we can directly represent and theoretically verify the correctness of discrete-time and continuous-time Simulink block diagrams. Moreover, we study the algebraic loop-free feedback composition with multistep delays.


## 3. Preliminary

In this section, we introduce some notations and notions that will be used in our work. We denote the set of natural numbers byN, i.e., 0,1,2,⋯, the set of positive integers by N+, i.e., 1,2,⋯, the set of positive real numbers R+, and the set of nonnegative real numbers by R0+. We denote the set of integers between 1 and n by n=1,⋯,n⊂N+. We denote vectors by bold fonts, and their components are indexed from 1 to n; for example, x=x1,⋯,xn, and xi is the i‐th component of x, i∈n.Following the definitions of vector addition and scalar multiplication in vector spaces, for two vectorsx=x1,x2 and y=y1,y2, the vector addition can be expressed as x+y=x1+y1,x2+y2 and the scalar multiplication can be expressed as kx1,x2=kx1,kx2, where k∈F and F is a field.We fix atime axisR0+. The continuous-time domain Tc is a subset of R0+ with a left endpoint equal to 0. The right endpoint may be open or closed. For any τ∈R+, the discrete-time domain is a set Tτ=tktk=kτ,k∈N, where the time instant tk is called sample time point, t0=0 is the initial time, and tk keeps increasing at every iteration, i.e., ∀k∈N,tk<tk+1.We denote then-dimensional real-valued vector space by Rn, where n∈N+. A signal is a function from a time-domain T to Z⊆Rn, i.e., z·:T↦Z (or z for short). We use ZT to denote a set of all signals z. A continuous-time signal is a signal defined over a continuous-time domain Tc. A discrete-time signal is a signal that is defined at the discrete-time domain Tτ. The values of the discrete-time signal update at each tk and remain constant in the intervals kτ,k+1τ,k∈N.


## 4. Simulink Block Diagrams and Semantics

In this section, we present the semantics of Simulink block diagrams. We will start by giving a brief introduction to Simulink block diagrams, and we highlight the features relevant to our work. For more details, we refer the reader to [3].


### 4.1. Introduction of Simulink Block Diagrams

A Simulink block diagram is a graphical representation of a dynamic system. The Simulink block diagrams are composed of blocks and wires. The blocks can be eitherelementary blocks provided by the Simulink library or composition blocks made up of elementary blocks or other composition blocks. An example that implements the relationship between the vehicle’s power, resistance, and speed is shown in Figure 2. It consists of Constant, Subsystem, and Scope, where Constant and Scope are elementary blocks, and the composition block Subsystem comprises four elementary blocks Gain1, Subtract, Integrator, and Gain2.Figure 2
A Simulink block diagram.In its most general form, theelementary block has Inputports and Outputports that receive the input signals and send the output signals. For some special blocks, the absence of Inputports or Outputports is also allowed. We will explain the details later. An elementary block is either stateful or stateless. We say a block is stateful if the output of this block depends on its inputs and internal states (i.e., memory). We say a block is stateless if the output depends only on its inputs. Wires transmit signals in the direction indicated by the arrow. It must transmit signals from Outputports of one block to Inputports of another block in terms of its sample times. An exception to this is that one wire can be drawn from another. This sends the original signal to two (or more) target blocks. Wire communication is instant. That is, when a block outputs the value to a wire, all blocks connected to that wire will see the new value simultaneously.To improve the modeling capabilities of Simulink, eachelementary block contains some user-tunable parameters. One of the significant parameters is sample time that indicates the rate at which the block executes in simulation. According to the sample time, the blocks are divided into two main categories: continuous and discrete blocks. The sample time comprises two parameters: sample time periodτ and initial time offsetθ. For the continuous blocks, the sample time periodτ=0. For the discrete blocks, the sample time periodτ is always greater than zero and less than the simulation end time and θ less than or equal to τ. Since the default value of the initial offset is 0, unless otherwise mentioned, we let the initial offset θ be 0. As an example, suppose that the time unit is seconds, let the sample time period of a block be 0.02 s, and then the block updates methods (update, derivative or output) each 0.02 s. The Simulink block diagrams can be single rate where all blocks run with the same period or multirate where blocks run on different periods. This work considers single rate discrete-time Simulink block diagrams and continuous-time Simulink block diagrams with τ=0.There are three basic composition operators in Simulink: (i) Serial composition is the composition that the output of the source block is connected to the input of the target block. (ii) Parallel composition is that two blocks are “stacked on top of each other” without any wires between the two blocks. (iii) Feedback composition is that the output of a block connects to one of its inputs. Other forms of composition can be assembled from these three basic composition operations and wires.


### 4.2. The Semantics of Simulink Block Diagrams

In this subsection, we formally define the semantics for Simulink block diagrams. We focus on the semantics ofelementary block, composition semantics for composition operators, and the semantics of communication between blocks.As introduced in 4.1, anelementary block has Inputports which receive the input signals, internal state, and Outputports that send the output signals. It describes a mathematical relationship between inputs, outputs, and internal states to capture dynamic behavior. We define an elementary block as a dynamical system.Definition 1 (An elementary block).
Anelementary blockB is a tuple x,s,y,φ,f, where
(i)
x:T↦X is an input signal, xt∈X⊆Rn, xt0 is the initial value of the input signal(ii)
y:T↦Y is an output signal, yt∈Y⊆Rm, yt0 is the initial value of the output signal(iii)
s:T↦S is an internal state signal, st∈S⊆Rp, st0 is the initial value of the internal state signal(iv)
φ is the transition function of internal state(v)
f is the output function, i.e., yt=fxt,stThe above definition can express bothdiscrete-time blocks and continuous-time blocks. We say that a block is continuous if it operates on continuous-time signals. We say a block is discrete if it operates on discrete-time signals. Every block must define its output function and may define initialize, update, or derivative function to realize the corresponding function. For the discrete-time blocks, we denote φ=φu, i.e., stk+1=φuxtk,stk, which refers to the update function of internal state. For the continuous-time blocks, we denote φ=φd, i.e., ṡt=φdxt,st, which refers to the derivative function of internal state. The input or internal state of a block can be empty, respectively. In that case, we denote the input or internal state by x=0 or s=0 and use a symbol “-” to denote the transition function of the internal state. If a block has no internal state, we say the block is stateless.Someelementary blocks mentioned in our article are shown in Table 1 Three simple examples are shown below.Example 1 (Unitdelay).
An example of a statefuldiscrete-time elementary block is the Unitdelay block. The Unitdelay expresses that the current output value of this block is equal to the value of the current internal state, and the value of the next internal state is equal to the current input value. It can be represented as Bu=xu,su,yu,sutk+1=xutk,yutk=sutk, where tk∈Tτ.Example 2 (Multistep delays).
A block with multistep delays is denoted asB=x,s,y,φ,f, where ytn·k=stn·k, and stn·k+1=xtn·k, where n means that the block outputs the input of this block after n sample periods, n∈N+,k∈N.Example 3 (Integrator).
An example of a statefulcontinuous-time elementary block is the Integrator. The block models the relations, ṡt=xt with yt=st. The Integrator can be represented as BI=xI,sI,yI,ṡIt=xIt,yIt=sIt, where t∈R0+.Table 1
The representation of someelementary blocks and their semantics.
LibraryDescriptionElementary blockSemanticsSourceConstantConstant valueB=0,0,y,−,yt=cSinksDisplaySystem outputB=x,0,y,−,yt=xtSignal routingSwitchConditional statementB=x,0,y,−,fyt=x1tx2t>0,x3tx2t≤0DiscreteUnitdelayDiscrete-time delayB=x,s,y,φ,fφ:stk+1=xtkf:ytk=stkDiscrete/continuousSine waveDiscrete-timeB=x,0,y,−,ytk=sinxtkMath operationsGainMath operationB=x,0,y,−,yt=3xtContinuousIntegratorContinuous-timeB=x,s,y,φ,fφ:ṡt=xt,f:yt=stMath operationsSumMath operationB=x,0,y,−,f,x=x1,x2yt=x1t+x2tMath operationsSubtractionMath operationB=x,0,y,−,f,x=x1,x2,yt=x1t−x2tMath operationsDivideMath operationB=x,0,y,−,yt=1xtWe use the observable trajectory to model the evolution of the input-output variables.Definition 2 (The observable trajectory of thediscrete-time elementary block).
LetB=x,s,y,φu,f be a discrete-time elementary block. An observable trajectory Tr of B is a set x,y:Tτ↦X×Y∃sytk=fstk,xtk∧stk+1=φuxtk,stk,k∈N, where x:Tτ↦X⊆Rn is the input trajectory and y:Tτ↦Y⊆Rmis the output trajectory.Definition 3 (The observable trajectory of thecontinuous-time elementary block).
LetB=x,s,y,φd,f be a continuous-time elementary block. An observable trajectory Tr of B is a set x,y:Tc↦X×Y∃syt=fst,xt∧ṡt=φdxt,st, where x:Tc↦X⊆Rn is the input trajectory and y:Tc↦Y⊆Rm is the output trajectory.The wires connect someOutputports of a block to some Inputports of other block for communicating. For any blocks, B1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, where x1=x1,1,⋯,x1,n, y1=y1,1,⋯,y1,m, x2=x2,1,⋯,x2,n, and y2=y2,1,⋯,y2,m. We model the wires between B1 and B2 as a relation, called unilateral connection. A unilateral connection is a set of variables pair y1,j,x2,i, for j∈m and i∈n, where the former of each pair is the output variable that comes from B1, the latter of each pair is the input variable that comes from B2. We define the unilateral connection as follows:Definition 4 (Unilateral connection).
Given two blocksB1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, we define a unilateral connection from B1 to B2 (and vice versa) as a relation ρ=y1,j,x2,ij∈m,i∈n satisfying that:
(i)
y1,j is the j‐th component of y1, for all j∈m(ii)
x2,i is the i‐th component of x2, for all i∈n(iii)
y1,jt=x2,it, for all t∈TNote that not all the blocks can be connected. Given a source blockB1=x1,s1,y1,φ1,f1 and a target block B2=x2,s2,y2,φ2,f2, if we connect the output variables of the source block with input variables of the target block, variable names and their types (the sets of values that a variable can take) impose some constraints: First, the names of the input and output variables should not conflict. Second, the types should match and Y1⊆X2, where Y1 is the type of y1 and X2 is the type of x2. Third, one output port can connect to many input ports, but an input port can connect to at most one output ports.For readability, we useρ1,⋯,ρn⊆ρ to denote a set of specific unilateral connection (determined by a relation as defined in Definition 4). Note that, since ρ=y1,j,x2,ij∈m,i∈n is a relation, we can also have ρy1,j=x2,iy1,j,x2,i∈ρ,j∈m,i∈n.


### 4.3. Composition

A Simulink block diagram is a composition block constructed byelementary blocks according to composition operators. We will define the semantics of three basic composition operators in the following, namely, serial, parallel, and algebraic loop-free feedback composition with multistep delays. We first consider the serial composition.We can compose blocksB1 and B2 to form a serial composition when there is a unilateral connection between B1 and B2 and the unilateral connection satisfies the connection rules, as shown in Figure 3(a).Definition 5 (Serial composition).
Given blocksB1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, a serial composition B1;B2ofB1 and B2 is defined as a block x,s,y,f,φ if there exists a unilateral connection and
x≔x1,s≔s1,s2,y≔y2,φ≔φ1x1,s1,φ2x2,s2,f≔f1;ρ;f2x,s=f2ρf1x1,s1,s2.
The definition of the serial composition ofelementary blocks coincides with the definition of an elementary block (i.e., Definition 1), and therefore a composition can be considered a block.Example 4 (Serial composition).
In Figure3(b), the stateless block Gain takes input x1, computes k∈R times of x1, and returns y1 as output, where x1:R↦R and y1:R↦R. Another stateless block Sum has the input x2=x2,1,x2,2 and output y2t=x2,1t+x2,2t, where x2:R↦R×R and y2:R↦R, ∀t∈R. Letρ be the unilateral connection between Gain and Sum. Then, we can express these blocks as follows:
Gain≔x1,0,y1,−,y1t=gainx1t,0,ρ≔y1,x2,1,y1,x2,2,Sum≔x2,0,y2,−,y2t=addx2t,0,where y2t=addx2t,0=x2,1t+x2,2t, y1t=gainx1t,0=k·x1t, y1t=x2,1t,y1t=x2,2t. According to Definition 5, we compute the output function of the serial composition as follows:
fx1t,0≔addρgainx1t,0=addρy1t,0=addx2t,0=x2,1t+x2,2t=2k·x1t.
Therefore, we haveGain;Adder≔x1,0,y2,−,y2t=2k·x1t.Figure 3
(a) Graphical representation of the serial composition of blocks, whereρ=y1,x2 is a unilateral connection between B1 and B2, the dashed box indicates a composition of blocks. (b) Graphical representation of an example of serial composition, where ρ=y1,x2,1,y1,x2,2 is a unilateral connection between Gain and Sum.
(a)(b)The serial composition of blocks satisfies associative laws.Lemma 6 (Associativity).
Given blocksB1, B2, and B3, we have B1;B2;B3=B1;B2;B3.Proof.
It is easy to verify using Definition5. Thus, if we compose multiple blocks in serial, we can first compose two blocks, compose the result with a third one, ⋯, and rearranging the brackets in the expression does not change the result as long as the block’s position remains the same.Parallel composition is a particular case of composition with connection, where theunilateral connection between B1 and B2 is an empty set. We define parallel composition as follows.Definition 7 (Parallel composition).
Given blocksB1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, we define the parallel composition B1B2 of B1 and B2 as a block x,s,y,f,φ, where
x≔x1,x2,s≔s1,s2,y≔y1,y2,φ≔φ1φ2x1,s1,x2,s2=φ1x1,s1,φ2x2,s2,f≔f1f2x1,s1,x2,s2=f1x1,s1,f2x2,s2.Example 5 (Parallel composition).
Consider the parallel composition shown in Figure4(a). The block Divide models the relation y1t=1/x1t, where x1 is the input signal and requires x1t≠0, y1 is the output signal, and t represents time. The Sine Wave block models the relation y2t=x2t, where x2 is the input variable and y2 is the output variable. Therefore, the Divide and Sine Wave can be represented as
Divide≔x1,0,y1,−,y1t=1x1t,SineWave≔x2,0,y2,−,y2t=x2t.
Following Definition7, we write the parallel composition as follows:
DivideSineWave≔x1,x2,0,y1,y2,−,y1t=1x1t,y2t=x2t.Figure 4
(a) Graphical representation of parallel composition, where the dashed box indicates a composition of blocks. (b) Graphical representation of a composition with serial and parallel, where the dashed box indicates a composition of blocks.
(a)(b)Note that Definition5 defines the case that all the Outputports of B1 match the Inputports of B2. However, not all Outputports of B1 match the Inputports of B2 and not all Outputports of B1 are connected to all the Inputports of B2. As an example, we consider Figure 4(b). To handle this composition, we introduce a particular elementary block Id representing its output is identical to its input. We model the wires that connect the y1,1 and x2,2 as Id1 and Id2, respectively. We then denote the composition by B=B1Id1;ρ;B1Id2, where ρ=y1,1,xId2,y1,2,x2,1,yId1,x2,2.The parallel composition of blocks satisfies commutative law and associative law.Lemma 8.
Given blocksB1, B2andB3, we have
(i)
B1B2=B2B1(ii)
B1B2B3=B1B2B3Proof.
Straightforward from the Definition7.We will next define the algebraic loop-free feedback composition with multistep delays. Before defining that, we first introduce the algebraic loop feedback to aid this definition. In Simulink, an algebraic loop occurs when an input port of a direct feedthrough block is driven by the output of the same block in the same time step. The direct feedthrough means that a stateless block computes its output only depending on the input value at the current time. In mathematics, an algebraic loop can be expressed as the algebraic equationfx,y=0, where x is the input variable and y is the algebraic variable. Simulink solves the algebraic equation for y at each time instant.A simple example of an algebraic loop is the feedback that represents in Figure5(a). The feedback is a Subtraction block with input x=x1,1,x1,2 and an output y. The first element x1,1 of input is used to communicate with the environment. The second element x1,2 is used for feedback. The output y is split into two equal signals: one is for output, and another is to feed the output back into input x1,2. Then, this loop implies that the output of the Subtraction block is an algebraic variable y that is constrained to equal the first input x1,1 minus x1,2, i.e., x1,1t−x1,2t=yt. Let x1,2t=yt and x1,1t=ut, we have ut−yt=yt, and then the solution of this loop is yt=ut/2.Figure 5
Graphical representation of feedback.
(a)(b)However, the algebraic loop has inherent difficulties in solving: (1) while Simulink solver solves the algebraic loop, the simulation can execute slowly. (2) Some algebraic loops have no solution (an example shown in Figure5(b), the expression of this loop is ut+yt=yt, etc. These problems lead to algebraic loops that are undesirable. To remove the algebraic loop, according to Simulink, we connect y to x1,2 by stateful blocks (such as Delay, Memory, or Integrator) in this feedback to break the algebraic loop. We refer to this kind of acyclic structure as algebraic loop-free feedback, as shown in Figure 6. The work [14] defined the feedback with Unitdelay. We will handle the case of multistep delays.Definition 9 (Algebraic loop-free feedback composition with multistep delays).
Let blocksB1=x1,s1,y1,φ1,f1 be feedback with an algebraic loop and B2=x2,s2,y2,φ2,f2 be a multistep delays block. Let ρ1=y2,x1,2 and ρ2=y,x2 be the unilateral connections between B1 and B2. We denote by B1⊗fB2 the algebraic loop-free feedback composition of B1 and B2 with multistep delays and define B1⊗fB2=x,s,y,φ,f, where
x≔x1,1,s=s1,s2,y=y1,φ≔φ1φ2x1,s1,x2,s2=φ1x1,s1,φ2x2,s2,f≔yt0t=t0,ytn·kt=tn·k,n,k∈N+.Figure 6
(a) Graphical representation of algebraic loop-free feedback composition with Unitdelay. (b) Graphical representation of algebraic loop-free feedback composition with Integrator.
(a)(b)In the definition above, the calculation process starts with the multistep delays block. Whent=t0, let the initial state st0=0,s2t0. The output’s initial value of this algebraic loop-free feedback yt0=f1x1,1t0,x1,2t0,st0. There exists ρ1, s.t. x1,2t0=ρ1y2t0, when y2t0=f2x2t0,s2t0. Given a delay step n∈N+, when t=tn·k, where k∈N, the output ytn·k=f1x1,1tn·k,x1,2tn·k,stn·k, where the internal state stn·k=0,s2tn·k, and x1,2tn·k=ρ1y2tn·k, where y2tn·k=f2x2tn·k,s2tn·k is the output of B2. There exists ρ2,s.t.x2tn·k=ρ2ytn·k−1 is the input of B2, and s2tn·k=φ2x2tn·k−1,s2tn·k−1.We next give an example to illustrate removing an algebraic loop by introducing Unitdelay, i.e., let the delay stepn=1.Example 6 (An algebraic loop-free feedback composition with Unitdelay).
In Figure6(a), the Sum block Sum=x1,1,x1,2,0,y1,−,y1t=x1,1t+x1,2t is feedback with an algebraic loop. We connect ytox1,2 in this feedback by the Unitdelay to break the algebraic loop. The Unitdelay block Bu=xu,su,yu,sutk+1=xutk,yutk=sutk, where tk∈Tτ. Let ρ1=yu,x1,2 and ρ2=y,xu, the ρ1 and ρ2 satisfy the connection rules, and then an algebraic loop-free feedback composition with Unitdelay is a block B1⊗fB2=x,s,y,φ,f, where x=x1,1,s=0,su,y=y, and the output function
yt=yt0t=t0,ytkt=tk,k∈N+.Whent=t0, let sut0 be the initial value of the internal state of the Unitdelay. We have yut0=sut0 and x1,2t0=yut0. Hence, we get the initial output value of this composition yt0=x1,1t0+sut0.Whent=tk,k∈N+, we first consider Unitdelay. Because of xutk=ytk, sutk+1=xutk,yutk=sutk, and x1,2tk=yutk, we have ytk=x1,1tk+ytk−1.Next, we give an example about algebraic loop-free feedback composition with Integrator.Example 7 (An algebraic loop-free feedback composition with Integrator).
An example of continuous time algebraic loop-free feedback composition with Integrator is shown in Figure6(b). As previously mentioned, the Sum block Sum=x1,1,x1,2,0,y1,−,y1t=x1,1t+x1,2t is feedback with an algebraic loop. The Integrator can be represented as BI=xI,sI,yI,ṡIt=xIt,yIt=sIt, where t∈R0+. In this composition, there exist unilateral connections ρ1=yI,x1,2 and ρ2=y,xI, and the unilateral connections satisfy the connection rules, and then an algebraic loop-free feedback composition with Integrator is a block B1⊗fB2=x,s,y,φ,f, where x=x1,1,s=0,sI. Let sI0 be the initial value of the internal state of the Integrator. We have yI0=sI0, and there is a ρ1, s.t. x1,20=yI0. Hence, we get y0=x1,10+x1,20=x1,10+yI0.
Whent∈R+, similarly, we first consider Integrator. Because there is a ρ2, s.t. xIt=yt, and ṡIt=xIt,yIt=sIt. There exists ρ1, s.t. x1,2t=yIt, we get
yt=x1,1t+x1,2t=x1,1t+yI0+∫0txIδdδ


## 4.1. Introduction of Simulink Block Diagrams

A Simulink block diagram is a graphical representation of a dynamic system. The Simulink block diagrams are composed of blocks and wires. The blocks can be eitherelementary blocks provided by the Simulink library or composition blocks made up of elementary blocks or other composition blocks. An example that implements the relationship between the vehicle’s power, resistance, and speed is shown in Figure 2. It consists of Constant, Subsystem, and Scope, where Constant and Scope are elementary blocks, and the composition block Subsystem comprises four elementary blocks Gain1, Subtract, Integrator, and Gain2.Figure 2
A Simulink block diagram.In its most general form, theelementary block has Inputports and Outputports that receive the input signals and send the output signals. For some special blocks, the absence of Inputports or Outputports is also allowed. We will explain the details later. An elementary block is either stateful or stateless. We say a block is stateful if the output of this block depends on its inputs and internal states (i.e., memory). We say a block is stateless if the output depends only on its inputs. Wires transmit signals in the direction indicated by the arrow. It must transmit signals from Outputports of one block to Inputports of another block in terms of its sample times. An exception to this is that one wire can be drawn from another. This sends the original signal to two (or more) target blocks. Wire communication is instant. That is, when a block outputs the value to a wire, all blocks connected to that wire will see the new value simultaneously.To improve the modeling capabilities of Simulink, eachelementary block contains some user-tunable parameters. One of the significant parameters is sample time that indicates the rate at which the block executes in simulation. According to the sample time, the blocks are divided into two main categories: continuous and discrete blocks. The sample time comprises two parameters: sample time periodτ and initial time offsetθ. For the continuous blocks, the sample time periodτ=0. For the discrete blocks, the sample time periodτ is always greater than zero and less than the simulation end time and θ less than or equal to τ. Since the default value of the initial offset is 0, unless otherwise mentioned, we let the initial offset θ be 0. As an example, suppose that the time unit is seconds, let the sample time period of a block be 0.02 s, and then the block updates methods (update, derivative or output) each 0.02 s. The Simulink block diagrams can be single rate where all blocks run with the same period or multirate where blocks run on different periods. This work considers single rate discrete-time Simulink block diagrams and continuous-time Simulink block diagrams with τ=0.There are three basic composition operators in Simulink: (i) Serial composition is the composition that the output of the source block is connected to the input of the target block. (ii) Parallel composition is that two blocks are “stacked on top of each other” without any wires between the two blocks. (iii) Feedback composition is that the output of a block connects to one of its inputs. Other forms of composition can be assembled from these three basic composition operations and wires.


## 4.2. The Semantics of Simulink Block Diagrams

In this subsection, we formally define the semantics for Simulink block diagrams. We focus on the semantics ofelementary block, composition semantics for composition operators, and the semantics of communication between blocks.As introduced in 4.1, anelementary block has Inputports which receive the input signals, internal state, and Outputports that send the output signals. It describes a mathematical relationship between inputs, outputs, and internal states to capture dynamic behavior. We define an elementary block as a dynamical system.Definition 1 (An elementary block).
Anelementary blockB is a tuple x,s,y,φ,f, where
(i)
x:T↦X is an input signal, xt∈X⊆Rn, xt0 is the initial value of the input signal(ii)
y:T↦Y is an output signal, yt∈Y⊆Rm, yt0 is the initial value of the output signal(iii)
s:T↦S is an internal state signal, st∈S⊆Rp, st0 is the initial value of the internal state signal(iv)
φ is the transition function of internal state(v)
f is the output function, i.e., yt=fxt,stThe above definition can express bothdiscrete-time blocks and continuous-time blocks. We say that a block is continuous if it operates on continuous-time signals. We say a block is discrete if it operates on discrete-time signals. Every block must define its output function and may define initialize, update, or derivative function to realize the corresponding function. For the discrete-time blocks, we denote φ=φu, i.e., stk+1=φuxtk,stk, which refers to the update function of internal state. For the continuous-time blocks, we denote φ=φd, i.e., ṡt=φdxt,st, which refers to the derivative function of internal state. The input or internal state of a block can be empty, respectively. In that case, we denote the input or internal state by x=0 or s=0 and use a symbol “-” to denote the transition function of the internal state. If a block has no internal state, we say the block is stateless.Someelementary blocks mentioned in our article are shown in Table 1 Three simple examples are shown below.Example 1 (Unitdelay).
An example of a statefuldiscrete-time elementary block is the Unitdelay block. The Unitdelay expresses that the current output value of this block is equal to the value of the current internal state, and the value of the next internal state is equal to the current input value. It can be represented as Bu=xu,su,yu,sutk+1=xutk,yutk=sutk, where tk∈Tτ.Example 2 (Multistep delays).
A block with multistep delays is denoted asB=x,s,y,φ,f, where ytn·k=stn·k, and stn·k+1=xtn·k, where n means that the block outputs the input of this block after n sample periods, n∈N+,k∈N.Example 3 (Integrator).
An example of a statefulcontinuous-time elementary block is the Integrator. The block models the relations, ṡt=xt with yt=st. The Integrator can be represented as BI=xI,sI,yI,ṡIt=xIt,yIt=sIt, where t∈R0+.Table 1
The representation of someelementary blocks and their semantics.
LibraryDescriptionElementary blockSemanticsSourceConstantConstant valueB=0,0,y,−,yt=cSinksDisplaySystem outputB=x,0,y,−,yt=xtSignal routingSwitchConditional statementB=x,0,y,−,fyt=x1tx2t>0,x3tx2t≤0DiscreteUnitdelayDiscrete-time delayB=x,s,y,φ,fφ:stk+1=xtkf:ytk=stkDiscrete/continuousSine waveDiscrete-timeB=x,0,y,−,ytk=sinxtkMath operationsGainMath operationB=x,0,y,−,yt=3xtContinuousIntegratorContinuous-timeB=x,s,y,φ,fφ:ṡt=xt,f:yt=stMath operationsSumMath operationB=x,0,y,−,f,x=x1,x2yt=x1t+x2tMath operationsSubtractionMath operationB=x,0,y,−,f,x=x1,x2,yt=x1t−x2tMath operationsDivideMath operationB=x,0,y,−,yt=1xtWe use the observable trajectory to model the evolution of the input-output variables.Definition 2 (The observable trajectory of thediscrete-time elementary block).
LetB=x,s,y,φu,f be a discrete-time elementary block. An observable trajectory Tr of B is a set x,y:Tτ↦X×Y∃sytk=fstk,xtk∧stk+1=φuxtk,stk,k∈N, where x:Tτ↦X⊆Rn is the input trajectory and y:Tτ↦Y⊆Rmis the output trajectory.Definition 3 (The observable trajectory of thecontinuous-time elementary block).
LetB=x,s,y,φd,f be a continuous-time elementary block. An observable trajectory Tr of B is a set x,y:Tc↦X×Y∃syt=fst,xt∧ṡt=φdxt,st, where x:Tc↦X⊆Rn is the input trajectory and y:Tc↦Y⊆Rm is the output trajectory.The wires connect someOutputports of a block to some Inputports of other block for communicating. For any blocks, B1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, where x1=x1,1,⋯,x1,n, y1=y1,1,⋯,y1,m, x2=x2,1,⋯,x2,n, and y2=y2,1,⋯,y2,m. We model the wires between B1 and B2 as a relation, called unilateral connection. A unilateral connection is a set of variables pair y1,j,x2,i, for j∈m and i∈n, where the former of each pair is the output variable that comes from B1, the latter of each pair is the input variable that comes from B2. We define the unilateral connection as follows:Definition 4 (Unilateral connection).
Given two blocksB1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, we define a unilateral connection from B1 to B2 (and vice versa) as a relation ρ=y1,j,x2,ij∈m,i∈n satisfying that:
(i)
y1,j is the j‐th component of y1, for all j∈m(ii)
x2,i is the i‐th component of x2, for all i∈n(iii)
y1,jt=x2,it, for all t∈TNote that not all the blocks can be connected. Given a source blockB1=x1,s1,y1,φ1,f1 and a target block B2=x2,s2,y2,φ2,f2, if we connect the output variables of the source block with input variables of the target block, variable names and their types (the sets of values that a variable can take) impose some constraints: First, the names of the input and output variables should not conflict. Second, the types should match and Y1⊆X2, where Y1 is the type of y1 and X2 is the type of x2. Third, one output port can connect to many input ports, but an input port can connect to at most one output ports.For readability, we useρ1,⋯,ρn⊆ρ to denote a set of specific unilateral connection (determined by a relation as defined in Definition 4). Note that, since ρ=y1,j,x2,ij∈m,i∈n is a relation, we can also have ρy1,j=x2,iy1,j,x2,i∈ρ,j∈m,i∈n.


## 4.3. Composition

A Simulink block diagram is a composition block constructed byelementary blocks according to composition operators. We will define the semantics of three basic composition operators in the following, namely, serial, parallel, and algebraic loop-free feedback composition with multistep delays. We first consider the serial composition.We can compose blocksB1 and B2 to form a serial composition when there is a unilateral connection between B1 and B2 and the unilateral connection satisfies the connection rules, as shown in Figure 3(a).Definition 5 (Serial composition).
Given blocksB1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, a serial composition B1;B2ofB1 and B2 is defined as a block x,s,y,f,φ if there exists a unilateral connection and
x≔x1,s≔s1,s2,y≔y2,φ≔φ1x1,s1,φ2x2,s2,f≔f1;ρ;f2x,s=f2ρf1x1,s1,s2.
The definition of the serial composition ofelementary blocks coincides with the definition of an elementary block (i.e., Definition 1), and therefore a composition can be considered a block.Example 4 (Serial composition).
In Figure3(b), the stateless block Gain takes input x1, computes k∈R times of x1, and returns y1 as output, where x1:R↦R and y1:R↦R. Another stateless block Sum has the input x2=x2,1,x2,2 and output y2t=x2,1t+x2,2t, where x2:R↦R×R and y2:R↦R, ∀t∈R. Letρ be the unilateral connection between Gain and Sum. Then, we can express these blocks as follows:
Gain≔x1,0,y1,−,y1t=gainx1t,0,ρ≔y1,x2,1,y1,x2,2,Sum≔x2,0,y2,−,y2t=addx2t,0,where y2t=addx2t,0=x2,1t+x2,2t, y1t=gainx1t,0=k·x1t, y1t=x2,1t,y1t=x2,2t. According to Definition 5, we compute the output function of the serial composition as follows:
fx1t,0≔addρgainx1t,0=addρy1t,0=addx2t,0=x2,1t+x2,2t=2k·x1t.
Therefore, we haveGain;Adder≔x1,0,y2,−,y2t=2k·x1t.Figure 3
(a) Graphical representation of the serial composition of blocks, whereρ=y1,x2 is a unilateral connection between B1 and B2, the dashed box indicates a composition of blocks. (b) Graphical representation of an example of serial composition, where ρ=y1,x2,1,y1,x2,2 is a unilateral connection between Gain and Sum.
(a)(b)The serial composition of blocks satisfies associative laws.Lemma 6 (Associativity).
Given blocksB1, B2, and B3, we have B1;B2;B3=B1;B2;B3.Proof.
It is easy to verify using Definition5. Thus, if we compose multiple blocks in serial, we can first compose two blocks, compose the result with a third one, ⋯, and rearranging the brackets in the expression does not change the result as long as the block’s position remains the same.Parallel composition is a particular case of composition with connection, where theunilateral connection between B1 and B2 is an empty set. We define parallel composition as follows.Definition 7 (Parallel composition).
Given blocksB1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2, we define the parallel composition B1B2 of B1 and B2 as a block x,s,y,f,φ, where
x≔x1,x2,s≔s1,s2,y≔y1,y2,φ≔φ1φ2x1,s1,x2,s2=φ1x1,s1,φ2x2,s2,f≔f1f2x1,s1,x2,s2=f1x1,s1,f2x2,s2.Example 5 (Parallel composition).
Consider the parallel composition shown in Figure4(a). The block Divide models the relation y1t=1/x1t, where x1 is the input signal and requires x1t≠0, y1 is the output signal, and t represents time. The Sine Wave block models the relation y2t=x2t, where x2 is the input variable and y2 is the output variable. Therefore, the Divide and Sine Wave can be represented as
Divide≔x1,0,y1,−,y1t=1x1t,SineWave≔x2,0,y2,−,y2t=x2t.
Following Definition7, we write the parallel composition as follows:
DivideSineWave≔x1,x2,0,y1,y2,−,y1t=1x1t,y2t=x2t.Figure 4
(a) Graphical representation of parallel composition, where the dashed box indicates a composition of blocks. (b) Graphical representation of a composition with serial and parallel, where the dashed box indicates a composition of blocks.
(a)(b)Note that Definition5 defines the case that all the Outputports of B1 match the Inputports of B2. However, not all Outputports of B1 match the Inputports of B2 and not all Outputports of B1 are connected to all the Inputports of B2. As an example, we consider Figure 4(b). To handle this composition, we introduce a particular elementary block Id representing its output is identical to its input. We model the wires that connect the y1,1 and x2,2 as Id1 and Id2, respectively. We then denote the composition by B=B1Id1;ρ;B1Id2, where ρ=y1,1,xId2,y1,2,x2,1,yId1,x2,2.The parallel composition of blocks satisfies commutative law and associative law.Lemma 8.
Given blocksB1, B2andB3, we have
(i)
B1B2=B2B1(ii)
B1B2B3=B1B2B3Proof.
Straightforward from the Definition7.We will next define the algebraic loop-free feedback composition with multistep delays. Before defining that, we first introduce the algebraic loop feedback to aid this definition. In Simulink, an algebraic loop occurs when an input port of a direct feedthrough block is driven by the output of the same block in the same time step. The direct feedthrough means that a stateless block computes its output only depending on the input value at the current time. In mathematics, an algebraic loop can be expressed as the algebraic equationfx,y=0, where x is the input variable and y is the algebraic variable. Simulink solves the algebraic equation for y at each time instant.A simple example of an algebraic loop is the feedback that represents in Figure5(a). The feedback is a Subtraction block with input x=x1,1,x1,2 and an output y. The first element x1,1 of input is used to communicate with the environment. The second element x1,2 is used for feedback. The output y is split into two equal signals: one is for output, and another is to feed the output back into input x1,2. Then, this loop implies that the output of the Subtraction block is an algebraic variable y that is constrained to equal the first input x1,1 minus x1,2, i.e., x1,1t−x1,2t=yt. Let x1,2t=yt and x1,1t=ut, we have ut−yt=yt, and then the solution of this loop is yt=ut/2.Figure 5
Graphical representation of feedback.
(a)(b)However, the algebraic loop has inherent difficulties in solving: (1) while Simulink solver solves the algebraic loop, the simulation can execute slowly. (2) Some algebraic loops have no solution (an example shown in Figure5(b), the expression of this loop is ut+yt=yt, etc. These problems lead to algebraic loops that are undesirable. To remove the algebraic loop, according to Simulink, we connect y to x1,2 by stateful blocks (such as Delay, Memory, or Integrator) in this feedback to break the algebraic loop. We refer to this kind of acyclic structure as algebraic loop-free feedback, as shown in Figure 6. The work [14] defined the feedback with Unitdelay. We will handle the case of multistep delays.Definition 9 (Algebraic loop-free feedback composition with multistep delays).
Let blocksB1=x1,s1,y1,φ1,f1 be feedback with an algebraic loop and B2=x2,s2,y2,φ2,f2 be a multistep delays block. Let ρ1=y2,x1,2 and ρ2=y,x2 be the unilateral connections between B1 and B2. We denote by B1⊗fB2 the algebraic loop-free feedback composition of B1 and B2 with multistep delays and define B1⊗fB2=x,s,y,φ,f, where
x≔x1,1,s=s1,s2,y=y1,φ≔φ1φ2x1,s1,x2,s2=φ1x1,s1,φ2x2,s2,f≔yt0t=t0,ytn·kt=tn·k,n,k∈N+.Figure 6
(a) Graphical representation of algebraic loop-free feedback composition with Unitdelay. (b) Graphical representation of algebraic loop-free feedback composition with Integrator.
(a)(b)In the definition above, the calculation process starts with the multistep delays block. Whent=t0, let the initial state st0=0,s2t0. The output’s initial value of this algebraic loop-free feedback yt0=f1x1,1t0,x1,2t0,st0. There exists ρ1, s.t. x1,2t0=ρ1y2t0, when y2t0=f2x2t0,s2t0. Given a delay step n∈N+, when t=tn·k, where k∈N, the output ytn·k=f1x1,1tn·k,x1,2tn·k,stn·k, where the internal state stn·k=0,s2tn·k, and x1,2tn·k=ρ1y2tn·k, where y2tn·k=f2x2tn·k,s2tn·k is the output of B2. There exists ρ2,s.t.x2tn·k=ρ2ytn·k−1 is the input of B2, and s2tn·k=φ2x2tn·k−1,s2tn·k−1.We next give an example to illustrate removing an algebraic loop by introducing Unitdelay, i.e., let the delay stepn=1.Example 6 (An algebraic loop-free feedback composition with Unitdelay).
In Figure6(a), the Sum block Sum=x1,1,x1,2,0,y1,−,y1t=x1,1t+x1,2t is feedback with an algebraic loop. We connect ytox1,2 in this feedback by the Unitdelay to break the algebraic loop. The Unitdelay block Bu=xu,su,yu,sutk+1=xutk,yutk=sutk, where tk∈Tτ. Let ρ1=yu,x1,2 and ρ2=y,xu, the ρ1 and ρ2 satisfy the connection rules, and then an algebraic loop-free feedback composition with Unitdelay is a block B1⊗fB2=x,s,y,φ,f, where x=x1,1,s=0,su,y=y, and the output function
yt=yt0t=t0,ytkt=tk,k∈N+.Whent=t0, let sut0 be the initial value of the internal state of the Unitdelay. We have yut0=sut0 and x1,2t0=yut0. Hence, we get the initial output value of this composition yt0=x1,1t0+sut0.Whent=tk,k∈N+, we first consider Unitdelay. Because of xutk=ytk, sutk+1=xutk,yutk=sutk, and x1,2tk=yutk, we have ytk=x1,1tk+ytk−1.Next, we give an example about algebraic loop-free feedback composition with Integrator.Example 7 (An algebraic loop-free feedback composition with Integrator).
An example of continuous time algebraic loop-free feedback composition with Integrator is shown in Figure6(b). As previously mentioned, the Sum block Sum=x1,1,x1,2,0,y1,−,y1t=x1,1t+x1,2t is feedback with an algebraic loop. The Integrator can be represented as BI=xI,sI,yI,ṡIt=xIt,yIt=sIt, where t∈R0+. In this composition, there exist unilateral connections ρ1=yI,x1,2 and ρ2=y,xI, and the unilateral connections satisfy the connection rules, and then an algebraic loop-free feedback composition with Integrator is a block B1⊗fB2=x,s,y,φ,f, where x=x1,1,s=0,sI. Let sI0 be the initial value of the internal state of the Integrator. We have yI0=sI0, and there is a ρ1, s.t. x1,20=yI0. Hence, we get y0=x1,10+x1,20=x1,10+yI0.
Whent∈R+, similarly, we first consider Integrator. Because there is a ρ2, s.t. xIt=yt, and ṡIt=xIt,yIt=sIt. There exists ρ1, s.t. x1,2t=yIt, we get
yt=x1,1t+x1,2t=x1,1t+yI0+∫0txIδdδ


## 5. A Contract-Based Refinement Approach

The correctness refers to the trajectories of Simulink block diagrams that should satisfy the requirement specifications of the system. Since contracts are centered around trajectories, they are expressive and versatile enough to specifydiscrete-time and continuous-time blocks. We use the contract as a specification language to formalize and prove system requirements and specify the trajectories of blocks. In this section, we present a generic contract-based method for proving the correctness of Simulink block diagrams with discrete-time and continuous-time blocks.Because the requirement specifications of a system are informal, we first formalize system requirement specifications into system contract specifications. We construct the Simulink block diagram according to the contract specification. We aim to prove that the Simulink block diagrams satisfy the system contract specification. To this end, the approach is divided into two steps. First, we modularly verify that Simulink block diagrams satisfy the composition contract (i.e., the composition of contracts corresponding to the blocks that construct the Simulink block diagrams). We associate a contract for every elementary block as a specification. After that, we define the satisfaction relation that relates block to contract and verify that the satisfaction relation is preserved by composition. That is, if blocks satisfy their contract, respectively, then the composition of blocks satisfies the composition of contracts. Second, we define the refinement relation between contracts and verify that the composition of contracts refines the system contract specifications. If the block diagram satisfies the composition contracts and the composition contracts refine the system specification, then the block diagram also satisfies the system specification. Hence, the Simulink block diagram is correct with respect to the system specification.We further elaborate on the concepts and properties mentioned above in the following. We first define the contract specification for the block.Definition 10 (Contract).
A contract is a tupleC=x,y,ϕa,ϕg, where
(i)
x,y are the input vectors and output vectors, respectively(ii)
ϕa⊆XT represents the assumption for the input trajectories of the block, where X⊆Rn(iii)
ϕg⊆X×YT represents the guarantee for the input-output trajectories of the block, where Y⊆RmThe contract specifies the expected trajectory for each elementary block. An example of a contract for a block Gain is shown below.Example 8 (Contract for Gain).
As an example, we consider the Gain block that represented in Example4. A contract specification for Gain is a tuple: C=x,y,ϕa,ϕg, where
ϕa≔x∈RT∀t∈T,xt∈R,ϕg≔x,y∈R×RT∀t∈T,yt=k·xt.Next, we will define the satisfaction relation, which relates a block to a contract by determining when a given block’s trajectories satisfy the specified specification. To define satisfaction relation, we first define a projection that expresses the input trajectory to aid that definition. A projection of a setTr⊆X×YT into X⊆XT is defined as the set Tr↓X=x∈X∃yx,y∈Tr, where T can be either the discrete-time domain or the continuous-time domain. We are now in a position to define satisfaction relation.Definition 11 (Satisfaction).
LetB=x,s,y,φ,f be a block and C=x,y,ϕa,ϕg be a contract. We say B satisfies C, denoted by B⊨C, if Tr↓X⊆ϕa and Tr⊆ϕg.We say thatB is a correct implementation of C if B⊨C. We have defined the notion of contract and satisfaction relation. The primary task of the proof method is to state that the satisfaction relation is preserved by composition. In the following, we study the composition operators of contracts according to the composition operators of blocks, i.e., serial, parallel, and algebraic loop-free feedback with multistep delays. We first define the serial composition of contracts.Definition 12 (The serial composition of contracts).
LetCi=xi,yi,ϕai,ϕgi be contracts for i=1,2. The serial composition of C1 and C2, written C1;C2, is a contract x,y,ϕa,ϕg, where
x=x1,y=y2,ϕa≔x1∈XTx1∈ϕa1∧∃y1x1,y1∈ϕg1∧ϕρ⟶y1∈ϕa2,ϕg≔x1,y2∈X×YT∃y1∃x2x1,y1∈ϕg1∧ϕρ∧x2,y2∈ϕg2,ϕρ≔∧y1,j,x2,i∈ρy1,jt=x2,it,∀t∈T.The serial composition preserves the satisfaction relation. That is, if blocks satisfy their contracts, respectively, then the composition of blocks satisfies the composition of contracts.Theorem 13 (Serial composition preserves satisfaction).
IfB1⊨C1 and B2⊨C2, then B1;B2⊨C1;C2.Proof.
We show a proof here for blocks withcontinuous-time trajectories, and the proof for blocks with discrete-time trajectories is similar. Let B1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2 be continuous-time blocks. The observable trajectories of B1 and B2 are denoted as Tr1=x1,y1:T↦X1×Y1∃s1y1=fx1,s1∧ṡ1=φd1x1,s1 and Tr2=x2,y2:T↦X2×Y2∃s2y2=fs2,x2∧ṡ2=φd2x2,s2, respectively, where X1,X2⊆Rn,Y1,Y2⊆Rm,n,m∈N+. The projection of Tr1 into X1 is Tr1↓X1=x1∃y1x1,y1∈Tr1. The projection of Tr2 into X2 is Tr2↓X2=x2∃y2x2,y2∈Tr2.
According to Definition5, we write B1;B2=x1,y2,s,f,φ. We denote the observable trajectories of B1;B2 by Tr. ThenTr=x1,y2∃sy2=f2ρf1x1,s1,s2∧ṡ=φdx,s. The projection of Tr into X1isTr↓X1=x1∃y1∃x2∃y2x1,y1∈Tr1∧y1,x2∈ρ∧x2,y2∈Tr2. So, Tr↓X1⊆Tr1↓X1.Given two contractsC1=x1,y1,ϕa1,ϕg1 and C2=x2,y2,ϕa2,ϕg2, by Definition 12, we have C1;C2=x1,y2,ϕa,ϕg, where ϕa=x1∈XTx1∈ϕa1∧∃y1x1,y1∈ϕg1∧ϕρ⟶y1∈ϕa2 and ϕg=x1,y2∈X×YT∃y1∃x2x1,y1∈ϕg1∧ϕρ∧x2,y2∈ϕg2.In order to proofB1;B2⊨C1;C2, according to Definition 11, we only need to show that: if Tr↓X1⊆ϕa implies Tr⊆ϕg. We first prove that Tr↓X1⊆ϕa.SinceB1⊨C1, according to Definition 11, we have Tr1↓X1⊆ϕa1 implies Tr1⊆ϕg1. That is, for all x1∈Tr↓X1⊆Tr1↓X1⊆ϕa1, then x1,y1∈ϕg1. Since B2⊨C2, according to Definition 11, we have for all x2∈Tr2↓X2⊆ϕa2, then Tr2⊆ϕg2. There exists a connection ρ=y1,x2, according to Definition 4, we have y1t=x2t. Then, y1∈ϕa2, and by the expression of ϕa, we have x1∈ϕa. Thus, Tr↓X1⊆ϕa. For all x1,y2∈Tr, we have x1,y1∈ϕg1, y1=x2, and x2,y2∈ϕg2. According to the expression of ϕg, we have x1,y2∈ϕg. Thus, Tr⊆ϕg. Hence, B1;B2⊨C1;C2.We now define the parallel composition of contracts.Definition 14 (The parallel composition of contracts).
Given contractsC1=x1,y1,ϕa1,ϕg1 and C2=x2,y2,ϕa2,ϕg2, we define the parallel composition of contracts as C1C2=x,y,ϕa,ϕg, where x=x1,x2,y=y1,y2, and
ϕa≔x∈XTx1∈ϕa1∧x2∈ϕa2,ϕg≔x,y∈X×YTx1,y1∈ϕg1∧x2,y2∈ϕg2.The parallel composition also preserves the satisfaction relation. That is, if blocks satisfy their contracts, respectively, then the parallel composition of blocks satisfies the parallel composition of contracts.Theorem 15 (Parallel composition preserves satisfaction).
IfB1⊨C1 and B2⊨C2, then B1B2⊨C1C2.Proof.
We show here a proof for blocks withcontinuous-time trajectories, and the proof for blocks with discrete-time trajectories is similar. Let B1=x1,s1,y1,φ1,f1 and B2=x2,s2,y2,φ2,f2 be blocks with continuous-time trajectories. The observable trajectories of B1 and B2 are denoted as Tr1=x1,y1:T↦X1×Y1∃s1y1=f1x1,s1∧ṡ1=φd1x1,s1 and Tr2=x2,y2:T↦X2×Y2∃s2y2=f2s2,x2∧ṡ2=φd2x2,s2, respectively, X1,X2⊆Rn,Y1,Y2⊆Rm,n,m∈N+. The projection of Tr1 into X1 is Tr1↓X1=x1∃y1x1,y1∈Tr1. The projection of Tr2 into X2 is the set Tr2↓X2=x2∃y2x2,y2∈Tr2. Following Definition 7, we write B1B2=x,y,s,f,φ. We denote the observable trajectories of B1B2 by Tr. Then Tr=x,y∃s=s1,s2y1=f1x1,s1∧ṡ1=φd1x1,s1∧y2=f2x2,s2∧ṡ2=φd2x2,s2. The projection of Tr into X is Tr↓X=x∃y1y2x1,y1∈Tr1∧x2,y2∈Tr2, where X⊆X1×X2T.
LetC1=x1,y1,ϕa1,ϕg1 and C2=x2,y2,ϕa2,ϕg2 be contracts. By Definition 14, we write C1C2=x,y,ϕa,ϕg, where x=x1,x2,y=y1,y2, and
(1)ϕa≔x∈XTx1∈ϕa1∧x2∈ϕa2,ϕg≔x,y∈X×YTx1,y1∈ϕg1∧x2,y2∈ϕg2.To proofB1B2⊨C1C2, according to Definition 11, we only need to show that if Tr↓X⊆ϕa implies Tr⊆ϕg. We first prove that Tr↓X⊆ϕa. Since B1⊨C1, according to Definition 11, we have if Tr1↓X1⊆ϕa1 implies Tr1⊆ϕg1. That is for all x1∈Tr1↓X1∈ϕa1, for all x1,y1∈Tr1, x1,y1∈ϕg1. Since B2⊨C2, we have Tr2↓X2⊆ϕa2 implies Tr2⊆ϕg2. That is, for all x2∈Tr2↓X2, then x2∈ϕa2, for all x2,y2∈Tr2, then x2,y2∈ϕg2. Hence, by (1), we have x=x1,x2∈ϕa, x,y∈ϕg. Hence, B1B2⊨C1C2.The parallel composition of contract is also associative and commutative.Lemma 16 (Associativity, commutativity).
LetC1, C2, and C3 be contracts. Then
(i)
C1C2=C2C1(ii)
C1C2C3=C1C2C3Proof.
Immediately follows from the Definition14.We now define the algebraic loop-free feedback composition of contracts.Definition 17 (The algebraic loop-free feedback composition of contracts).
LetC1=x1,y1,ϕa1,ϕg1 and C2=x2,y2,ϕa2,ϕg2 be the contracts. The algebraic loop-free feedback composition of C1 and C2 be defined as C1⊗fC2=x,y,ϕa,ϕg, where x=x1,1,y=y1, and
ϕa≔x1,1∈XTx1,1∈ϕa1∧∃y1x1,y1∈ϕg1∧ϕρ2⟶y1∈ϕa2∧∃y2x2,y2∈ϕg2∧ϕρ1⟶y2∈ϕa1,ϕg≔x1,1,y1∈X×YT∃x1,2∃y2∃x2x1,y1∈ϕg1∧ϕρ∧x2,y2∈ϕg2,ϕρ≔ϕρ1∧ϕρ2.where ϕρ2≔∧y1,j,x2,i∈ρ2y1,jt=x2,it,ϕρ1≔∧y2,j,x1,i∈ρ1y2,jt=x1,it, and x1=x1,1,x1,2.The algebraic loop-free feedback composition also preserves the satisfaction relation.Theorem 18 (Algebraic loop-free feedback composition preserves satisfaction).
LetB1 be the feedback with an algebraic loop and B2 be a block with multistep delays. Let C1=x1,y1,ϕa1,ϕg1 and C2=x2,y2,ϕa2,ϕg2 be the contracts. If B1⊨C1 and B2⊨C2, then B1⊗fB2⊨C1⊗fC2.Proof.
It easily follows from Theorem13 to Theorem 15.We next turn to the refinement relation between the contract. We follow a standard notion inspired by [20].Definition 19 (Refinement of contracts).
LetC1=x,y,ϕa1,ϕg1 and C2=x,y,ϕa2,ϕg2 be two contracts. We say C2 refines C1, denoted by C2≼C1, ifϕa1⊆ϕa2 and ϕg2⊆ϕg1.Refinement relaxes assumptions and reinforces guarantees, therefore, strengthening the contract. Obviously, the following refinement rule holds.Lemma 20.
LetC1=x,y,ϕa1,ϕg1 and C2=x,y,ϕa2,ϕg2 be two contracts. Then
(i)
Ci≼Ci, for i=1,2(ii)
Ifϕa1⊆ϕa2 and ϕg2=ϕg1, then C2≼C1(iii)
Ifϕg2⊆ϕg1 and ϕa1=ϕa2, then C2≼C1The refinement implies that every Simulink block diagram satisfies theC2 also satisfies the C1. This gives us the following property of correctness.Theorem 21 (Correctness).
LetB=x,s,y,φ,f be a block. Let C1=x,y,ϕa1,ϕg1 and C2=x,y,ϕa2,ϕg2 be contracts. The B is said to be correct for C2, if B⊨C1∧C1≼C2⇒B⊨C2.
Proof. SupposeC1≼C2, in terms of Definition 19, then ϕa2⊆ϕa1, and ϕg1⊆ϕg2. Suppose B⊨C1, then, for all x∈Tr↓X⊆ϕa1, and Tr⊆ϕg1⊆ϕg2. Hence, if x∈Tr↓X⊆ϕa2, then B⊨C2.Theorem21 is essential in our contract theory since it relates the Simulink block diagram (composition block) to a system contract specification. That is, if a Simulink block diagram satisfies the composition contract, and the composition contract refines the system contract, then it also satisfies the system contract. This ensures that the Simulink block diagram is correct.


## 6. Case Study

We have discussed the proof approach in the previous section, and in this section, the approach that we proposed is being implemented through a real-world case study.


### 6.1. Problem Statement

We examine a case, a safety-critical water level control system of reservoir, to illustrate how to verify that the controller model of a reservoir originating from the farmland irrigation satisfy the safety requirements.This reservoir mainly is used for irrigation and considers the comprehensive utilization of flood control and aquaculture. An inlet water pipe and a spillway exist on the top and bottom of the dam, respectively. The maximum dam height is40m, the maximum is 30m, and the minimum water level is 10m. The management facilities of the reservoir are very backward. There are no special management agencies to observe and safety check the water level and no timely flood control.We will use Simulink to model the water level control system of the reservoir and simulate the water level trajectories to monitor the water level control operation. Then we adopt the method that we presented to verify the Simulink block diagram’s correctness for ensuring the water level’s safety according to the reservoir’s actual situation. The water level controls the opening or closing of the valves. That is, the water level is neither higher than the highest water level, which causes the dam to be overloaded, nor can the aquaculture industry and farmland irrigation be affected by the water level being lower than the lowest water level.


### 6.2. Architectural Overview of Control System

The control system of water level consists of the following two major components: Sensor and Plant.(i)
Sensor. The Sensor is a water level sensor. Inputs about the water level of the reservoir from its corresponding level sensor, and we suppose that the Sensor works properly(ii)
Plant. The Plant is made up of four principal components, as shown in Figure 7(a): Reservoir, Valves, Controller, and Water inlet and outlet pipe
(a)
Reservoir. The Reservoir has parameters giving the maximum water lever L2, the minimum water lever L1, and the water level of the reservoir h≥0(b)
Water valves. The Reservoir has two water valves. The inlet valve V2 is at the top of the Reservoir, and the outlet valve V1 is at the bottom. We suppose that the valves are either fully opened or fully closed immediately(c)
Controller. The Controller is able to read the current water level provided by the sensor, and the output is the command signal open or closed. The controller’s target is to keep the water level between the minimum water lever L1 and the maximum water lever L2(d)
Water inlet and outlet. The inlet pipe Fin≥0 and Fout≥0, and Fin≠Fout.Figure 7
(a) An overview of reservoir system. (b) The model of controller.
(a)(b)As the system is a closed-loop system, the controller must work with the reservoir. In Figure8(a), a system including both controller and plant is given. We only focus on the controller.Figure 8
(a) A Simulink block diagram of reservoir system. (b) The block diagram of controller.
(a)(b)


### 6.3. The Safety Requirements of Water Level

The safety requirements for water levelh in the controller are given below, and the purpose is to avoid the water empty and filling of reservoir.Requirement 1 When theh of reservoir is above L1, the V1 is opened, and when the h of reservoir is below L1, the V1 is closed.Requirement 2 When theh of reservoir is above L2, the V2 is closed, and when the h of reservoir is below L2, the V2 is opened.Driven by requirement, we now refine system-level requirements into block-level implementations. When the system is refined, subsystem details are added. We first decompose the controller into three different controllers:Decision controller, Controller1 controller, and Controller2 controller. The block diagrams of these controllers can be depicted graphically as in Figure 8(b). In the block diagram, the Decision decides that the water level is high or low. The Controller1 computes whether the Valve1 should be open, while the Controller2 computes if the Valve2 should be open.For theDecision, if the water level is above L2, it is high. If the water level is below L1, it is low. For the Valve2, if the water level is high, then Valve2 should be close(0). Otherwise, the Valve2 should be open(1). For the Valve1, if the water level is low, then Valve1 should be close(0). Otherwise, then Valve1 should be open(1).We use the contract as a formal specification language. We supposeL1=10m, L2=30m, and 0m≤ht≤40m. The system-level safety requirement specification 1 is denoted as Creq1=h,yv1,ϕareq1,ϕgreq1.
(2)ϕareq1≔h∈RT∀t∈T,0≤ht≤40,ϕgreq1≔h,yv1∈R×RT∀t∈T,yv1=open1,ht≥10,close0,0≤ht<10..The system-level safety requirement specification 2 is denoted asCreq2=h,yv2,ϕareq2,ϕgreq2, where
(3)ϕareq2≔h∈RT∀t∈T,0≤ht≤40,ϕgreq2≔h,yv2∈R×RT∀t∈T,yv2=close0,ht≥30,open1,0≤ht<30..


### 6.4. Verification of Correctness for the Controller System

We construct a Simulink block diagram for the control system according to requirements shown in Figure7(b). Following the previous technical route, the verification method applied in this case consists of two stages.Stage 1: verifying the Simulink block diagram satisfies the corresponding composition of contract.TheDecision controller has two controllers: Decision1 and Decision2. The Decision2 determines whether the water level is higher than the highest water level. The composition of Simulink block diagrams of Decision2 is denoted as ⊗Bd2=Bc1Bc0;ρ1;Bsw1, where ρ1=yc1,sw11,yc0,sw13. We denote the h by sw12, and then ⊗Bd2≔sw12,0,yd2,−,fd2sw12t,0, where,
(4)fd2sw12,0=1highsw12t≥30,0¬highsw12t<30.Therefore, the observable trajectories of⊗Bd2 are denoted as Tr2=sw12,yd2:T↦R×R∀t∈T,yd2t=fd2sw12t,0, where
(5)yd2t=1highsw12t≥30,0¬highsw12t<30.The main task in the next step is to apply the composition rules to calculate the composition contract and prove that the composition of blocks satisfies the composition of the corresponding contracts. We first specify a contract for each elementary block following Table1. Then we apply the composition rules to calculate the composition contract and prove that the composition of blocks satisfies the composition contracts.The composition contract of theDecision2 is stated as ⊗Cd2=sw12,yd2,ϕad2,ϕgd2, where
(6)ϕad2≔sw12∈RT∀t∈T,∃yB1:0,yB1∈ϕgB1∧ϕρ1⟶yB1∈ϕaBsw1,ϕgd2≔0,yd2∈R×RT∀t∈T,0,yB1∈ϕgB1∧ϕρ1∧sw12,yd2∈ϕgsw1,ϕρ1≔yc1t=sw11t∧yc0t=sw13t.Since(7)ϕgB1≔0,yB1∈R2×R2T∀t∈T,yc1t=1∧yc0t=0,ϕgBsw1≔sw12,yd2∈R×RT∀t∈T,yd2t=fsw1sw12t,0,where
(8)yd2t=sw11sw12≥30,sw13sw12<30.We use quantifier elimination law to simplify the expression. Therefore, the composition contract⊗Cd2 of the Decision2 controller was written in the following form.
(9)ϕad2≔sw12∈RT∀t∈T,sw12t∈R,ϕgd2≔sw12,yd2∈R×RT∀t∈T,yd2t=high1sw12t≥30,¬high0sw12t<30..Similarly, theDecision1 determines whether the water level is below the lowest water level. The composition of Simulink block diagrams of Decision1 is denoted as ⊗Bd1=Bc1Bc0;ρ2;Bs′w1, where ρ2=yc0,s′w11,yc1,s′w13. Let B1=Bc1Bc0 and yB1=yc0,yc1. We denote the Simulink block diagrams of Decision1 by ⊗Bd1≔s′w12,0,yd1,−,fd1s′w12t,0, where
(10)fd1s′w12t,0=0¬lows′w12t≥10,1lows′w12t<10.The observable trajectories of⊗Bd1 is denoted as Tr1=s′w12,yd1:T↦R×R∀t∈T,yd1t=fd1s′w12t,0, where
(11)yd1t=0¬lows′w12t≥10,1lows′w12t<10.The composition contract of theDecision1 controller for ⊗Bd1 is stated as ⊗Cd1=s′w12,yd1,ϕad1,ϕgd1, where
(12)ϕad1≔s′w12∈RT∀t∈T,s′w12t∈R,ϕgd1≔s′w12,yd1∈R×RT∀t∈T,l@l@yd1t=¬low0s′w12t≥10,low1s′w12t<10..Since variablessw12 and s′w12 are used to read the values of water level, so sw12t=ht and s′w12t=ht. According to Definition 11, ∀t∈T, we have sw12∈RTsw12t≥0⊆ϕad2, Tr2⊆ϕgd2, and s′w12∈RTs′w12t≥0⊆ϕad1, Tr1⊆ϕgd1. Hence, ⊗Bd2⊨⊗Cd2 and ⊗Bd1⊨⊗Cd1.We next turn to research the controllerController1. It can be represented as a composition block ⊗Bv1=Bc1Bc0;ρ3;Bs′w2, where ρ3=yc1,s′w23,yc0,s′w21. Let ⊗Bv1=s′w22,0,yv1,−,yv1t=fv1s′w22t,0, where
(13)fv1s′w22t,0=0closes′w22t>0,1opens′w22t≤0.Therefore, the observable trajectories of⊗Bv1 is denoted as Tr3=s′w22,yv1:T↦R×R∀t∈T,yv1t=fv1s′w22t,0, where
(14)yv1t=0closes′w22t>0,1opens′w22t≤0.The composition contract ofController1 is stated as ⊗Cv1=s′w22,yv1,ϕav1,ϕgv1, where
(15)ϕav1≔s′w22∈RT∀t∈T,s′w22t∈R,ϕgv1≔s′w22,yv1∈R×RT∀t∈T′,yv1s′w22t,0=0closes′w22t>0,1opens′w22t≤0..According to Definition11, ∀t∈T, we have s′w22:T↦Rs′w22t∈R⊆ϕav1, and Tr3⊆ϕgv1. Hence, ⊗Bv1⊨⊗Cv1.For requirement 1 Next, we will compose theDecision1 controller and Controller1 controller for verifying requirement 1. We denote the composition of Decision1 and Controller1 by ⊗BIm1. We denote the h by s′w12. We write ⊗BIm1=⊗Bd1;⊗Bv1=s′w12,0,yv1,−,yv1=fIm1s′w12t,0, where
(16)fIm1s′w12t,0=1opens′w12t≥10,0closes′w12t<10.The observable trajectories of⊗BIm1 is denoted as TrIm1=s′w12,yv2:T↦R×R∀t∈T,yIm1t=fIm1s′w12t,0, where
(17)yIm1t=1opens′w12t≥10,0closes′w12t<10.The composition contract of⊗BIm1 is defined as ⊗CIm1=s′w12,yv1,ϕaIm1,ϕgIm1, and
(18)ϕaIm1≔s′w12∈RT∀t∈T,s′w12t∈R,ϕgIm1≔s′w12,yv1∈R×RT∀t∈T,yv1t=1opens′w12t≥10,0closes′w12t<10..∀t∈T, we have s′w12t:T↦Rs′w12t∈R⊆ϕaIm1, and TrIm1⊆ϕgIm1. Hence, BIm1⊨CIm1.Stage 2: correctness verification. Our primary goal in this step is to verify that the Simulink block diagram⊗Bv1 is correct for system contract Creq1. In terms of Definition 19, we get ϕareq1⊆ϕaIm1 and ϕgIm1⊆ϕgreq1, then, CIm1≼Creq1. According to Theorem 21, we have BIm1⊨CIm1∧CIm1≼Creq1⇒BIm1⊨Creq1.For requirement 2We next turn to verify the correctness of the Simulink block diagrams for requirement 2. Similar to the method above, theController2 controller can be represented as a composition block ⊗Bv2= Bc1Bc0;ρ4;Bsw2, where ρ4=yc1,sw23,yc0,sw21. Then ⊗Bv2=sw22,0,yv2,−,yv2t=fv2sw22t,0, where
(19)yv2t=0close,sw22t>0,1open,sw22t≤0.Therefore, the observable trajectories of the subsystem⊗Bv2 is denoted as Tr4=sw22,yv2:T↦R×R∀t∈T,yv2t=fv2sw22t,0, where
(20)yv2t=0close,sw22t>0,1open,sw22t≤0.Stage 1: verifying the Simulink block diagram satisfies the corresponding composition of contract.The composition contract ofController2 is defined as ⊗Cv2=sw22,yv2,ϕav2,ϕgv2, where
(21)ϕav2≔sw22∈RT∀t∈T,sw22t∈R,ϕgv2≔sw22,yv2∈R×RT∀t∈T,yv2t=0close,sw22t>0,1open,sw22t≤0..According to Definition11, ∀t∈T, we have sw22t∈RTsw22t∈R⊆ϕav2, and Tr4⊆ϕgv2. Hence, ⊗Bv2⊨⊗Cv2.Next, we will compose theDecision2 and Controller2 to verify requirement 2. Let ⊗BIm2=⊗Bd2;⊗Bv2=sw12,0,yv2,−,yv2=fv2sw12t,0, where
(22)fIm2sw12t,0=0close,sw12t≥30,1open,sw12t>30.The observable trajectories of⊗BIm2 are denoted as TrIm2=sw12,yv2:T↦R×R∀t∈T,yIm2t=fIm2sw12t,0, where
(23)yIm2t=0close,sw12t≥30,1open,sw12t<30.The composition contract is defined as⊗CIm2=sw22,yv2,ϕaIm2,ϕgIm2, and
(24)ϕaIm2≔sw12∈RT∀t∈T,sw12t∈R,ϕgIm2≔sw12,yv2∈R×RT∀t∈T′,yv2sw12t,0=0close,sw12t≥30,1open,sw12t<30..Stage 2: correctness verification. Our main goal in this step is to verify that the Simulink block diagram (⊗Bv2) is a correct implementation of system contract Creq2. ∀t∈T, we have sw12t:T↦Rsw12t∈R⊆ϕaIm2, and TrIm2⊆ϕgIm2. Hence, BIm2⊨CIm2. In terms of Definition 19, we get ϕareq2⊆ϕaIm2,ϕgIm2⊆ϕgreq2. Then, CIm2≼Creq2. According to Theorem 21, we have BIm2⊨CIm2∧CIm2≼Creq2⇒BIm2⊨Creq2.In the example above, when an attacker adds a malicious logic bomb to Simulink, it can maliciously manipulate the input and output behaviors of any block in the block diagrams and the water level values read from the Sensor. This may lead to the block diagram’s behavior not satisfying the system’s formal specification. Considering from this perspective, our approach can identify and verify whether the designed CPS is planted with the logic bomb.


## 6.1. Problem Statement

We examine a case, a safety-critical water level control system of reservoir, to illustrate how to verify that the controller model of a reservoir originating from the farmland irrigation satisfy the safety requirements.This reservoir mainly is used for irrigation and considers the comprehensive utilization of flood control and aquaculture. An inlet water pipe and a spillway exist on the top and bottom of the dam, respectively. The maximum dam height is40m, the maximum is 30m, and the minimum water level is 10m. The management facilities of the reservoir are very backward. There are no special management agencies to observe and safety check the water level and no timely flood control.We will use Simulink to model the water level control system of the reservoir and simulate the water level trajectories to monitor the water level control operation. Then we adopt the method that we presented to verify the Simulink block diagram’s correctness for ensuring the water level’s safety according to the reservoir’s actual situation. The water level controls the opening or closing of the valves. That is, the water level is neither higher than the highest water level, which causes the dam to be overloaded, nor can the aquaculture industry and farmland irrigation be affected by the water level being lower than the lowest water level.


## 6.2. Architectural Overview of Control System

The control system of water level consists of the following two major components: Sensor and Plant.(i)
Sensor. The Sensor is a water level sensor. Inputs about the water level of the reservoir from its corresponding level sensor, and we suppose that the Sensor works properly(ii)
Plant. The Plant is made up of four principal components, as shown in Figure 7(a): Reservoir, Valves, Controller, and Water inlet and outlet pipe
(a)
Reservoir. The Reservoir has parameters giving the maximum water lever L2, the minimum water lever L1, and the water level of the reservoir h≥0(b)
Water valves. The Reservoir has two water valves. The inlet valve V2 is at the top of the Reservoir, and the outlet valve V1 is at the bottom. We suppose that the valves are either fully opened or fully closed immediately(c)
Controller. The Controller is able to read the current water level provided by the sensor, and the output is the command signal open or closed. The controller’s target is to keep the water level between the minimum water lever L1 and the maximum water lever L2(d)
Water inlet and outlet. The inlet pipe Fin≥0 and Fout≥0, and Fin≠Fout.Figure 7
(a) An overview of reservoir system. (b) The model of controller.
(a)(b)As the system is a closed-loop system, the controller must work with the reservoir. In Figure8(a), a system including both controller and plant is given. We only focus on the controller.Figure 8
(a) A Simulink block diagram of reservoir system. (b) The block diagram of controller.
(a)(b)


## 6.3. The Safety Requirements of Water Level

The safety requirements for water levelh in the controller are given below, and the purpose is to avoid the water empty and filling of reservoir.Requirement 1 When theh of reservoir is above L1, the V1 is opened, and when the h of reservoir is below L1, the V1 is closed.Requirement 2 When theh of reservoir is above L2, the V2 is closed, and when the h of reservoir is below L2, the V2 is opened.Driven by requirement, we now refine system-level requirements into block-level implementations. When the system is refined, subsystem details are added. We first decompose the controller into three different controllers:Decision controller, Controller1 controller, and Controller2 controller. The block diagrams of these controllers can be depicted graphically as in Figure 8(b). In the block diagram, the Decision decides that the water level is high or low. The Controller1 computes whether the Valve1 should be open, while the Controller2 computes if the Valve2 should be open.For theDecision, if the water level is above L2, it is high. If the water level is below L1, it is low. For the Valve2, if the water level is high, then Valve2 should be close(0). Otherwise, the Valve2 should be open(1). For the Valve1, if the water level is low, then Valve1 should be close(0). Otherwise, then Valve1 should be open(1).We use the contract as a formal specification language. We supposeL1=10m, L2=30m, and 0m≤ht≤40m. The system-level safety requirement specification 1 is denoted as Creq1=h,yv1,ϕareq1,ϕgreq1.
(2)ϕareq1≔h∈RT∀t∈T,0≤ht≤40,ϕgreq1≔h,yv1∈R×RT∀t∈T,yv1=open1,ht≥10,close0,0≤ht<10..The system-level safety requirement specification 2 is denoted asCreq2=h,yv2,ϕareq2,ϕgreq2, where
(3)ϕareq2≔h∈RT∀t∈T,0≤ht≤40,ϕgreq2≔h,yv2∈R×RT∀t∈T,yv2=close0,ht≥30,open1,0≤ht<30..


## 6.4. Verification of Correctness for the Controller System

We construct a Simulink block diagram for the control system according to requirements shown in Figure7(b). Following the previous technical route, the verification method applied in this case consists of two stages.Stage 1: verifying the Simulink block diagram satisfies the corresponding composition of contract.TheDecision controller has two controllers: Decision1 and Decision2. The Decision2 determines whether the water level is higher than the highest water level. The composition of Simulink block diagrams of Decision2 is denoted as ⊗Bd2=Bc1Bc0;ρ1;Bsw1, where ρ1=yc1,sw11,yc0,sw13. We denote the h by sw12, and then ⊗Bd2≔sw12,0,yd2,−,fd2sw12t,0, where,
(4)fd2sw12,0=1highsw12t≥30,0¬highsw12t<30.Therefore, the observable trajectories of⊗Bd2 are denoted as Tr2=sw12,yd2:T↦R×R∀t∈T,yd2t=fd2sw12t,0, where
(5)yd2t=1highsw12t≥30,0¬highsw12t<30.The main task in the next step is to apply the composition rules to calculate the composition contract and prove that the composition of blocks satisfies the composition of the corresponding contracts. We first specify a contract for each elementary block following Table1. Then we apply the composition rules to calculate the composition contract and prove that the composition of blocks satisfies the composition contracts.The composition contract of theDecision2 is stated as ⊗Cd2=sw12,yd2,ϕad2,ϕgd2, where
(6)ϕad2≔sw12∈RT∀t∈T,∃yB1:0,yB1∈ϕgB1∧ϕρ1⟶yB1∈ϕaBsw1,ϕgd2≔0,yd2∈R×RT∀t∈T,0,yB1∈ϕgB1∧ϕρ1∧sw12,yd2∈ϕgsw1,ϕρ1≔yc1t=sw11t∧yc0t=sw13t.Since(7)ϕgB1≔0,yB1∈R2×R2T∀t∈T,yc1t=1∧yc0t=0,ϕgBsw1≔sw12,yd2∈R×RT∀t∈T,yd2t=fsw1sw12t,0,where
(8)yd2t=sw11sw12≥30,sw13sw12<30.We use quantifier elimination law to simplify the expression. Therefore, the composition contract⊗Cd2 of the Decision2 controller was written in the following form.
(9)ϕad2≔sw12∈RT∀t∈T,sw12t∈R,ϕgd2≔sw12,yd2∈R×RT∀t∈T,yd2t=high1sw12t≥30,¬high0sw12t<30..Similarly, theDecision1 determines whether the water level is below the lowest water level. The composition of Simulink block diagrams of Decision1 is denoted as ⊗Bd1=Bc1Bc0;ρ2;Bs′w1, where ρ2=yc0,s′w11,yc1,s′w13. Let B1=Bc1Bc0 and yB1=yc0,yc1. We denote the Simulink block diagrams of Decision1 by ⊗Bd1≔s′w12,0,yd1,−,fd1s′w12t,0, where
(10)fd1s′w12t,0=0¬lows′w12t≥10,1lows′w12t<10.The observable trajectories of⊗Bd1 is denoted as Tr1=s′w12,yd1:T↦R×R∀t∈T,yd1t=fd1s′w12t,0, where
(11)yd1t=0¬lows′w12t≥10,1lows′w12t<10.The composition contract of theDecision1 controller for ⊗Bd1 is stated as ⊗Cd1=s′w12,yd1,ϕad1,ϕgd1, where
(12)ϕad1≔s′w12∈RT∀t∈T,s′w12t∈R,ϕgd1≔s′w12,yd1∈R×RT∀t∈T,l@l@yd1t=¬low0s′w12t≥10,low1s′w12t<10..Since variablessw12 and s′w12 are used to read the values of water level, so sw12t=ht and s′w12t=ht. According to Definition 11, ∀t∈T, we have sw12∈RTsw12t≥0⊆ϕad2, Tr2⊆ϕgd2, and s′w12∈RTs′w12t≥0⊆ϕad1, Tr1⊆ϕgd1. Hence, ⊗Bd2⊨⊗Cd2 and ⊗Bd1⊨⊗Cd1.We next turn to research the controllerController1. It can be represented as a composition block ⊗Bv1=Bc1Bc0;ρ3;Bs′w2, where ρ3=yc1,s′w23,yc0,s′w21. Let ⊗Bv1=s′w22,0,yv1,−,yv1t=fv1s′w22t,0, where
(13)fv1s′w22t,0=0closes′w22t>0,1opens′w22t≤0.Therefore, the observable trajectories of⊗Bv1 is denoted as Tr3=s′w22,yv1:T↦R×R∀t∈T,yv1t=fv1s′w22t,0, where
(14)yv1t=0closes′w22t>0,1opens′w22t≤0.The composition contract ofController1 is stated as ⊗Cv1=s′w22,yv1,ϕav1,ϕgv1, where
(15)ϕav1≔s′w22∈RT∀t∈T,s′w22t∈R,ϕgv1≔s′w22,yv1∈R×RT∀t∈T′,yv1s′w22t,0=0closes′w22t>0,1opens′w22t≤0..According to Definition11, ∀t∈T, we have s′w22:T↦Rs′w22t∈R⊆ϕav1, and Tr3⊆ϕgv1. Hence, ⊗Bv1⊨⊗Cv1.For requirement 1 Next, we will compose theDecision1 controller and Controller1 controller for verifying requirement 1. We denote the composition of Decision1 and Controller1 by ⊗BIm1. We denote the h by s′w12. We write ⊗BIm1=⊗Bd1;⊗Bv1=s′w12,0,yv1,−,yv1=fIm1s′w12t,0, where
(16)fIm1s′w12t,0=1opens′w12t≥10,0closes′w12t<10.The observable trajectories of⊗BIm1 is denoted as TrIm1=s′w12,yv2:T↦R×R∀t∈T,yIm1t=fIm1s′w12t,0, where
(17)yIm1t=1opens′w12t≥10,0closes′w12t<10.The composition contract of⊗BIm1 is defined as ⊗CIm1=s′w12,yv1,ϕaIm1,ϕgIm1, and
(18)ϕaIm1≔s′w12∈RT∀t∈T,s′w12t∈R,ϕgIm1≔s′w12,yv1∈R×RT∀t∈T,yv1t=1opens′w12t≥10,0closes′w12t<10..∀t∈T, we have s′w12t:T↦Rs′w12t∈R⊆ϕaIm1, and TrIm1⊆ϕgIm1. Hence, BIm1⊨CIm1.Stage 2: correctness verification. Our primary goal in this step is to verify that the Simulink block diagram⊗Bv1 is correct for system contract Creq1. In terms of Definition 19, we get ϕareq1⊆ϕaIm1 and ϕgIm1⊆ϕgreq1, then, CIm1≼Creq1. According to Theorem 21, we have BIm1⊨CIm1∧CIm1≼Creq1⇒BIm1⊨Creq1.For requirement 2We next turn to verify the correctness of the Simulink block diagrams for requirement 2. Similar to the method above, theController2 controller can be represented as a composition block ⊗Bv2= Bc1Bc0;ρ4;Bsw2, where ρ4=yc1,sw23,yc0,sw21. Then ⊗Bv2=sw22,0,yv2,−,yv2t=fv2sw22t,0, where
(19)yv2t=0close,sw22t>0,1open,sw22t≤0.Therefore, the observable trajectories of the subsystem⊗Bv2 is denoted as Tr4=sw22,yv2:T↦R×R∀t∈T,yv2t=fv2sw22t,0, where
(20)yv2t=0close,sw22t>0,1open,sw22t≤0.Stage 1: verifying the Simulink block diagram satisfies the corresponding composition of contract.The composition contract ofController2 is defined as ⊗Cv2=sw22,yv2,ϕav2,ϕgv2, where
(21)ϕav2≔sw22∈RT∀t∈T,sw22t∈R,ϕgv2≔sw22,yv2∈R×RT∀t∈T,yv2t=0close,sw22t>0,1open,sw22t≤0..According to Definition11, ∀t∈T, we have sw22t∈RTsw22t∈R⊆ϕav2, and Tr4⊆ϕgv2. Hence, ⊗Bv2⊨⊗Cv2.Next, we will compose theDecision2 and Controller2 to verify requirement 2. Let ⊗BIm2=⊗Bd2;⊗Bv2=sw12,0,yv2,−,yv2=fv2sw12t,0, where
(22)fIm2sw12t,0=0close,sw12t≥30,1open,sw12t>30.The observable trajectories of⊗BIm2 are denoted as TrIm2=sw12,yv2:T↦R×R∀t∈T,yIm2t=fIm2sw12t,0, where
(23)yIm2t=0close,sw12t≥30,1open,sw12t<30.The composition contract is defined as⊗CIm2=sw22,yv2,ϕaIm2,ϕgIm2, and
(24)ϕaIm2≔sw12∈RT∀t∈T,sw12t∈R,ϕgIm2≔sw12,yv2∈R×RT∀t∈T′,yv2sw12t,0=0close,sw12t≥30,1open,sw12t<30..Stage 2: correctness verification. Our main goal in this step is to verify that the Simulink block diagram (⊗Bv2) is a correct implementation of system contract Creq2. ∀t∈T, we have sw12t:T↦Rsw12t∈R⊆ϕaIm2, and TrIm2⊆ϕgIm2. Hence, BIm2⊨CIm2. In terms of Definition 19, we get ϕareq2⊆ϕaIm2,ϕgIm2⊆ϕgreq2. Then, CIm2≼Creq2. According to Theorem 21, we have BIm2⊨CIm2∧CIm2≼Creq2⇒BIm2⊨Creq2.In the example above, when an attacker adds a malicious logic bomb to Simulink, it can maliciously manipulate the input and output behaviors of any block in the block diagrams and the water level values read from the Sensor. This may lead to the block diagram’s behavior not satisfying the system’s formal specification. Considering from this perspective, our approach can identify and verify whether the designed CPS is planted with the logic bomb.


## 7. Conclusion and Future Work

In this paper, we presented a method to prove the correctness of Simulink block diagrams withdiscrete-time or continuous-time blocks using contract. This approach addressed the problem of proving that the system formal specifications are satisfied by composition and refinement of trajectories. We showed the usability of our proposals via a use case (as an example) which models the control system of a reservoir. Our method can improve the reliability of Simulink and reduce the development costs by performing early safety verification on verification of the target system.In this work, we made the first step towards the contract-based verification of cyber-physical models in Simulink. Future work includes extending the work along several dimensions. First, this work considers single rate Simulink block diagrams. We will extend this work to consider the multiple sample times (multirate systems) diagrams. Another nontrivial extension involves applying our idea to prove the correctness of Simulink block diagrams mixture ofdiscrete-time and continuous-time blocks. More challenging would be to develop a contract-based refinement approach to handle Stateflow. Second, this work only considers the blocks whose inputs-outputs can be explicitly represented through the mathematical relation. It is interesting to prove the correctness of the Simulink block diagrams, whose input-output behavior be expressed implicitly by a mathematical relation. Third, we plan to automatically verify the correctness of the Simulink block diagrams based on our method.



---

*Source: 8015896-2022-09-19.xml*