Xiong Xu

Bohua Zhan

Shuling Wang

Jean-Pierre Talpin

Naijun Zhan

A denotational semantics of Simulink with higher-order UTP

Keywords: model-based design, cyber-physical systems, unifying theory of programming, denotational semantics, Mathworks Simulink

Matlab/Simulink is a de-facto industrial standard for modelling embedded systems. Reflecting the complexity of cyber-physical system (CPS) design, the semantics of Simulink is complex, mixing discrete and continuous time and events. In this paper, we define a compositional semantics of hierarchical Simulink diagrams using Higher-order Unifying Theories of Programming (HUTP) for CPS design. The HUTP theory satisfies the suitable algebraic properties to serve as a mathematical foundation for expressing the semantics of CPSs, in particular Simulink diagrams. We characterise a class of well-formed Simulink diagrams and prove the determinacy of their HUTP semantics. Moreover, we construct a framework for proving the consistency between Simulink diagrams and their translation to HCSP (Hybrid Communicating Sequential Processes). Finally, we provide a case study to illustrate and justify this translation.

Introduction

Cyber-Physical Systems (CPSs) are networked computing units controlling physical plants as diverse as grids, factories, supply chains, ground, sea, air and space transportation systems. CPSs are complex to design, verify and maintain, while often entrusted safety-critical roles. The efficient and verified development of safe and reliable CPSs is hence a priority mandated by many standards, yet a notoriously difficult and challenging field of engineering and research. Matlab/Simulink is a de-facto industrial standard for modelling cyber-physical systems. Reflecting the complexity of CPS design, Simulink is known to have a complex semantics, which need to describe interactions between discrete and continuous time behaviors, trigger events, hierarchical structure, and so on.

Model-based design (MBD) [START_REF] Gajski | Embedded System Design: Modeling, Synthesis, Verification[END_REF] has long become a predominant approach to break down the difficulties and challenges in CPS design into abstracted and comprehensible elements. Hoare and He's Unifying Theories of Programming (UTP) [START_REF] Hoare | Unifying Theories of Programming[END_REF] is built upon the mathematical foundations of theorem proving and has both the core simplicity and the necessary extensibility to capture models of imperative and concurrent software, hardware, and physics found in CPS design under a common relational calculus suitable for design and verification.

Hybrid systems, which could be subsumed in the domain of CPSs, seamlessly integrate discrete behavior with continuous dynamical systems, and have been extended to capture probabilistic, stochastic, time-delayed behaviours and even more complex features. In previous works (Xu et al., 2022a), we defined one such conservative extension to Hoare and He's UTP theory with higher-order quantification, i.e., the Higher-order UTP (HUTP), to provide a formal semantics for modelling and verifying hybrid systems, mixing discrete real-time processes and continuous dynamics. Within HUTP, we defined a calculus of normal hybrid designs to model and analyse hybrid systems. A normal hybrid design describes a contract between the component and its environment, and therefore supports the decomposition of engineering tasks to resolve system design complexity. Normal hybrid designs as a firstclass notion in the HUTP theory enjoys some desired algebraic properties, and therefore can serve as a semantic foundation for CPS design.

In (Zou et al., 2013b[START_REF] Zou | Formal verification of Simulink/Stateflow diagrams[END_REF], we introduced methods for translation of Simulink and Stateflow diagrams to Hybrid Communicating Sequential Processes (HCSP), in order to verify them using the Hybrid Hoare Logic prover implemented in Isabelle/HOL (Zou et al., 2013a;[START_REF] Wang | An improved HHL prover: an interactive theorem prover for hybrid systems[END_REF]. The correctness of the translation can be proved using HUTP. Concretely, we define the respective HUTP semantics for Simulink and HCSP, and then compare the HUTP representations of Simulink diagrams and their HCSP models to check the semantic consistency. In (Xu et al., 2022a), we defined a formal semantics for Simulink based on normal hybrid designs. However, the normal-hybrid-design semantics is complex, which pose difficulties for ensuing analysis and verification. The complexity comes from (1) involvement of a large number of communications (including the communications between atomic discrete blocks), and (2) the use of normal hybrid design, although intuitive for system design, makes the definitions long and cumbersome. Moreover, compositional semantics for hierarchical Simulink subsystems is not considered.

Therefore, we introduce in this paper a new compositional formalisation of denotational semantics for hierarchical Simulink diagrams based on HUTP, featuring both discrete and continuous behaviours, as well as composition using normal, enabled and triggered subsystems. The expressivity of the present denotational semantics is well-suited for verifying correctness of translation from Simulink to other formalisms, such as HCSP (Zou et al., 2013b), differential dynamic logic [START_REF] Liebrenz | Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X[END_REF] and hybrid automata [START_REF] Agrawal | Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations[END_REF]. We exercise this capability by constructing a framework for proving the semantic consistency between Simulink diagrams and their corresponding HCSP models, and provide a case study to demonstrate and justify our translation of Simulink into HCSP.

In summary, the main contributions of this paper comprise:

• A notion of Simulink processes and their parallel composition based on conjunction of relations, which simplifies the HUTP theory for Simulink;

• A denotational semantics for hierarchical Simulink diagrams based on Simulink processes, reflecting the composability of subsystems and therefore following the principle of modular design;

• Notions of well-formedness of Simulink diagrams, and proof of semantic determinacy for these diagrams;

• A framework for proving correctness of translation from Simulink to HCSP, which is illustrated with a simple case study.

Paper Organisation. The rest of the paper is organised as follows. Section 2 retrospects some preliminary concepts of Simulink, UTP and Higher-order UTP. Section 3 defines the notion of Simulink processes which serve as the semantic foundation for Simulink. Starting from Simulink blocks, Section 4 defines the HUTP semantics for Simulink diagrams by Simulink processes, and proves determinacy of the semantics for well-formed diagrams. Section 5 defines the compositional HUTP semantics for hierarchical Simulink diagrams containing normal, triggered and enabled subsystems. In Section 6, we illustrate by a case study how to prove the semantic consistency between Simulink diagrams and the corresponding HCSP models. Section 7 addresses the related work and Section 8 concludes this paper and discusses future work.

Preliminaries

In this section, we will present the preliminaries on Simulink, classical UTP, and our previous work on the higher-order UTP for hybrid systems.

Simulink

Simulink (MathWorks, 2013) is a widely-used design environment for building embedded control systems, with support for graphical modelling and efficient numerical simulation. Dynamic systems, possibly combining continuous and discrete behaviors, can be modelled by Simulink block diagrams. A rich set of fixed-step and variable-step solvers is provided for simulating dynamic systems. Fig. 1 shows how a simple plant-control system can be modelled in Simulink. Blocks are the basic units for building Simulink models. Each block is defined with input and output ports, an output method that defines how the output values are calculated, optional internal states and corresponding update methods that define how the states are changed. It may also contain user-defined parameters that alter the functionality, such as the symbol parameter "+-" for Add block, resulting in Subtract; the parameter of threshold for Switch block, and so on. Sample time is one of the most important parameters of a block and specifies the rate of execution when the block executes the output method and the update method (if it exists). Among the different types of sample time, three basic ones are frequently used: discrete with sample time st for some st > 0, continuous with sample time 0, and inherited. For the inherited case, the sample time is not defined explicitly, but instead determined from the context of the corresponding block through a process called sample time propagation. For instance, if the sample times of all the input signals of an inherited block are known, then sample time of the block is computed as the greatest common divisor of the sample times of these input signals. According to sample time, blocks can be categorised into two kinds: discrete and continuous blocks. Simulink provides discrete and continuous solvers to compute the states of blocks at each time step respectively.

Blocks are connected using lines to transfer signals from one block to another. The signals are time-varying and can be considered as functions mapping from real time to values. For discrete blocks the functions are piecewise constant. Blocks in a diagram may have different sample times, e.g. a multi-rate discrete system with discrete blocks that sample at different rates, or a hybrid continuous and discrete system. For such diagrams, the simulator must meet the precision specified on the continuous states, and hit all the sample times for the discrete states. The simulator needs to sort (or schedule) the blocks to be executed in a certain order. This may not be possible if there are algebraic loops in the diagram, in which case the diagram may be considered to be invalid. The blocks which maintain state variables such as the Integrator or Unit Delay blocks can break the loop.

Blocks can be grouped into subsystems to establish a hierarchical structure on Simulink diagrams. We consider three types of subsystems: normal subsystems, triggered subsystems and enabled subsystems. A normal subsystem executes as a single unit within the model. It can specify its system sample time and its execution is equivalent to executing the blocks inside the subsystem. Both triggered and enabled subsystems are conditionally executed subsystems. A triggered subsystem is defined with inherited sample time, that runs when the trigger signal is rising, falling, or either (rising or falling) through a zero value. An enabled subsystem runs when its control signal is positive.

A hierarchical Simulink model is thus composed of blocks, subsystems, and lines between them. After a Simulink model is built, it is ready for simulation. Each step of simulation corresponds to one sample time of the overall diagram. At each step, first compute the internal state and output of each block by invoking the corresponding output and update methods in the correct order; second, choose appropriate ODE solvers to compute evolution of continuous blocks through time. If there are triggered subsystems or integrator blocks with resets, zero crossings may need to be computed. The process ends when the given simulation time is reached.

Unifying Theories of Programming

Hoare and He's Unifying Theories of Programming (UTP) [START_REF] Hoare | Unifying Theories of Programming[END_REF] is an alphabetised refinement calculus unifying heterogeneous programming paradigms. An alphabetised relation consists of an alphabet α(P ), containing its variables x and primes x , and a relational predicate P referring to this vocabulary. The terms x and x are called observable variables:

x is observable at the start of execution and x is observable at the end of execution. The behaviour of a program is encoded as a relation between the observable variables x and x . In particular, assignment, sequential composition, conditional statement, non-deterministic choice, and recursion of imperative programs can be specified as alphabetised relations below, where x and x are sequences or vectors of variables, x\{x} (x \{x }) denotes excluding x (x ) from x (x ). To start with, the relational calculus comprises all operators of first-order logic.

x := e = x = e ∧ x \{x } = x\{x} P Q = ∃x * • P [x * /x ] ∧ Q[x * /x] P b Q = (b ∧ P ) ∨ (¬b ∧ Q) P Q = P ∨ Q P Q = P ∧ Q
Conventionally, is an algebraic sibling for ∧ and for ∨. In the equal tradition of UTP [START_REF] Hoare | Unifying Theories of Programming[END_REF]Xu et al., 2022a), however, they denote ∨ and ∧, respectively. We will follow UTP's convention in this paper.

Assignment x := e is defined by observing the update x of variable x once its value e is evaluated, leaving other variables in the alphabet x unchanged. Sequence P Q is modelled by locally binding, through x * , the final state x of P and the initial state x of Q, both of which are instantiated to x * . Note that requires α out (P ) = α in (Q), where α out (P ) and α in (Q) denote the sets of output and input variables in α(P ) and α(Q), respectively, and α in (Q) is the primed version by priming all the variables in α in (Q). The conditional P b Q evaluates as P if b is true and as Q otherwise. P Q non-deterministically chooses P or Q, and P Q is a conjunction of P and Q.

Let P and Q be two predicates with the same alphabet, say {x, x }.

Then, Q is a refinement of P , denoted P Q, if ∀x, x • Q ⇒ P . In addition, P Q iff P Q = P iff P Q = Q.
With respect to the refinement order , the least (µ) and greatest (ν) fixed points of a function F between programs can be defined as follows:

µF = {X | F (X) X} νF = {X | X F (X)}
The notion of healthiness conditions plays an important role in the UTP theory. If a predicate satisfies P = H(P ), then it is said to be H-healthy. In other words, a healthiness condition H defines an invariant predicate set {X | H(X) = X}, and is required to be idempotent (H • H = H), which means that taking the medicine twice leaves you as healthy as taking it once (no overdoses). So, in UTP, the healthy predicates of a theory are the fixed points of idempotent functions. When H is monotonic on a complete lattice (C, ), then according to the Knaster-Tarski theorem [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF], the UTP theory satisfying H forms a complete lattice {X ∈ C | H(X) = X}. Additionally, recursion can be well defined. Distinct healthiness conditions can be composed to capture the characteristics of different programming paradigms. Concretely, a programming paradigm can be defined by a collection of healthiness conditions

H 1 , H 2 , • • •, H n . Their com- position H 1 • H 2 • • • • • H n
forms the semantic model of the domain-specific paradigm under consideration. For example, in Section 3.1, we introduce healthiness conditions characterising Simulink processes.

The higher-order UTP for hybrid systems

Higher-order UTP (HUTP) (Xu et al., 2022a) is a conservative extension to Hoare and He's UTP theory which supports the specification of discrete, real-time and continuous dynamics, concurrency and communication, and higher-order quantification. In (Xu et al., 2022a), we defined a formal semantics for Simulink based on a notion of normal hybrid designs. However, this semantics is complex and difficult to analyse for reasons given in Section 1. In this paper, we instead consider an abstracted HUTP semantics for Simulink, based on the notion of abstract hybrid processes proposed in (Xu et al., 2022a) as future work. While having weaker algebraic structure than normal hybrid designs (e.g., chaos is not a left zero of sequential composition), abstract hybrid processes are simpler, of sufficient expressivity to define a semantics of Simulink, and are more comfortable for verification.

Abstract hybrid processes

As mentioned in (Xu et al., 2022a), HUTP separates the concerns in hybrid system design into time, state and trace. We introduce the notion of time by two observational variables ti , ti : R ≥0 ∪ {+∞} to specify the startand end-time of the observed behaviour. The notion of state is represented by real-time variables and their derivatives, which are functions over time, and differential relations over them that are very powerful to express all kinds of continuous dynamics. Therefore, there are three versions for each state variable v:

• v ∈ D stands for its initial value in the domain D, where D could be a Banach space;

• the primed version v ∈ D stands for the final value, i.e., the output state variable; and

• the real time version Timed traces tr and tr record the execution history and capture communication behaviours, where tr represents the timed trace before the process is started and tr stands for timed trace up to the moment of observation. However, in this paper, no communication is involved and the parallel composition is based on shared variables, so timed traces are abstracted away, which is the main feature of abstract hybrid processes.

We use the boldface symbols v, v , ∼ v and ∼ v to denote respective vectors of input, output, real-time state variables and their derivatives. The alphabet our theory depends on is {ti , ti , v, ∼ v, ∼ v, v } by default. Therefore, first-order predicate P (x, x ) used in classical UTP [START_REF] Hoare | Unifying Theories of Programming[END_REF] can be extended to higher-order differential relation

∼ P (ti , ti , v, ∼ v, ∼ v, v
). However, not all higher-order differential relations are expected, such as ti > ti indicating time going backwards. Thus, we use healthiness conditions to exclude the ill behaviours. As introduced in (Xu et al., 2022a), the features of abstract hybrid processes can be captured by the following four healthiness conditions (H 1 is defined for traces, hence not applicable for abstract hybrid processes):

• Time must be irreversible:

H a 0 (X) = X ∧ ti ≤ ti
• If the preceding process does not terminate, i.e., ti = +∞, the current process should do nothing but keep the time observation unchanged, i.e.,

H a 2 (X) = (ti = ti ) ti = +∞ X where P b Q = (b ∧ P ) ∨ (¬b ∧ Q).
• If the current process does not terminate, i.e., ti = +∞, the values of the output state variables are unobservable, i.e.,

H a 3 (X) = (∃v • X) ti = +∞ X
• If the process evolves for a period of time, i.e., ti < ti , the real-time value ∼ v should stay right-continuous (RC) and semi-differentiable (SD). Let v k , ∼ v k , and v k denote the k-th variable in v, ∼ v k , and v k , respectively. Then, we define

RC = ∀k • ∀t ∈ [ti , ti ) • ∃d • ∼ v k (t) = lim δ→0 + ∼ v k (t + δ) = d SD = ∀k • ∀t ∈ (ti , ti ) • ∃d 0 • lim δ→0 + ( ∼ v k (t + δ) - ∼ v k (t)) /δ = d 0 ∧∃d 1 • lim δ→0 -( ∼ v k (t + δ) - ∼ v k (t)) /δ = d 1
The healthiness condition

H 4 (X) = X ∧ RC ∧ SD
rules out some ill behaviours, such as the Dirichlet function (returning 1 if t is a rational number and 0 otherwise) and the Weierstrass function (continuous everywhere but differentiable nowhere).

Remark 1. Note that H a 3 does not mean that the values of v exist at infinity. The existential quantifier just indicates that the output v can take arbitrary values, i.e., chaos. In addition, the output of a process exhibiting Zenobehaviour should also be unobservable (chaos). However, it cannot be captured by abstract hybrid processes as the trace information is abstracted away.

An abstract hybrid process is a fixed point of X = H a HP (X), where

H a HP = H a 0 • H a 2 • H a 3 • H 4
It is proved in (Xu et al., 2022a) that H a HP is idempotent and monotonic, which indicates that abstract hybrid processes form a complete lattice under the refinement order .

Simulink processes in HUTP

Based on abstract hybrid processes, we propose a new notion of Simulink processes which can serve as the semantic foundation for Simulink. We further define parallel composition of Simulink processes as conjunction of relations. Finally, we define some syntactic sugar to simplify the ensuing presentations.

Simulink processes

The semantics of Simulink can be represented by a subset of abstract hybrid processes subject to additional healthiness conditions. First, we assume that the execution of Simulink diagrams will consume time (ti < ti ). This corresponds to the requirement that simulation will last for non-zero amount of time. Moreover, we require that simulations will always terminate (ti < +∞). These two properties can be captured by the following healthiness condition:

H SIM (X) = X ∧ ti < ti < +∞ It can be proved that H SIM is idempotent and monotonic, which indicates that H a SIM = H SIM • H a
HP also forms a complete lattice under the refinement order. We call the H a SIMhealthy relations Simulink processes, and we prove the following property, which reveals that H a 0 , H a 2 and H a 3 are redundant and therefore simplifies the representation of Simulink processes.

Property 2. H a SIM ≡ H SIM • H 4 Proof. It can be checked that H SIM • H a 0 (X) = H SIM • H a 2 (X) = H SIM • H a 3 (X) = H SIM (X).
We next describe the meet ( , ∨), join ( , ∧) and sequential composition ( ) operations on Simulink processes. They are specializations of corresponding operations for general hybrid processes defined in (Xu et al., 2022a). The sequential composition of two Simulink processes P and Q is defined as follows:

P Q = ∃ti 0 , v 0 • P[ti 0 , v 0 /ti , v ] ∧ Q[ti 0 , v 0 /ti , v]
provided that α out (P) = α in (Q), where α out (P) and α in (Q) denote the sets of output and input variables in the respective alphabets of P and Q, and α in (Q) is the primed version by priming all the variables in α in (Q). If α out (P) = α in (Q), then we can extend the alphabets by

α + out (P) = α + in (Q) = α out (P) ∪ α in (Q)
to ensure the well-definedness of . The meet and join operations simply correspond to union and intersection of relations. We then prove , ∨ and ∧ are H a SIM -preserving, and the proofs for other operations on Simulink processes are similar.

Property 3. If P and Q are H a SIM -healthy, so are P Q, P ∨ Q, and P ∧ Q.

Proof. By the definition of H a SIM ,

P Q = 0 < ti < ti < +∞ ∧ P ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) 0 < ti < ti < +∞ ∧ Q ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) = ∃ti 0 , v 0 • 0 < ti < ti 0 < +∞ ∧ 0 < ti 0 < ti < +∞ ∧P[ti 0 , v 0 /ti , v ] ∧ Q[ti 0 , v 0 /ti , v] ∧RC ( ∼ v, ti , ti 0 ) ∧ RC ( ∼ v, ti 0 , ti ) ∧ SD( ∼ v, ti , ti 0 ) ∧ SD( ∼ v, ti 0 , ti ) = ∃ti 0 , v 0 • 0 < ti < ti 0 < ti < +∞ ∧P[ti 0 , v 0 /ti , v ] ∧ Q[ti 0 , v 0 /ti , v] ∧RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti )
where RC and SD denote ∼ v is right continuous and semi-differentiable as specified in healthiness condition H 4 . We can also prove

P ∨ Q = 0 < ti < ti < +∞ ∧ P ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) ∨ 0 < ti < ti < +∞ ∧ Q ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) = 0 < ti < ti < +∞ ∧ (P ∨ Q) ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) P ∧ Q = 0 < ti < ti < +∞ ∧ P ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) ∧ 0 < ti < ti < +∞ ∧ Q ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) = 0 < ti < ti < +∞ ∧ (P ∧ Q) ∧ RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti )
According to the above results, we can prove that P Q, P ∨ Q and P ∧ Q are H a SIM -healthy.

Parallel composition

Of all the operations, parallel composition is the most important. In (Xu et al., 2022a), we assume that the state variables of different processes are disjoint. Based on this assumption, a parallel-by-merge scheme is given. In this paper, we relax this assumption: state variables can be shared among processes. Intuitively, the combination is well-behaved because although variables are shared, the value of each variable is controlled by at most one process and only read by others. Hence, under some additional assumptions, we can prove that there exists unique assignment to all variables given the values of input variables to the overall process.

Therefore, the parallel-by-merge scheme (Fig. 1 of (Xu et al., 2022a)) can be revisited to represent the parallel composition by shared state variables in this paper. The parallel-by-merge, originated from [START_REF] Hoare | Unifying Theories of Programming[END_REF], is a typical scheme to define parallel composition in UTP (Xu et al., 2022a;[START_REF] Foster | Unifying theories of reactive design contracts[END_REF]. Intuitively, parallel processes first execute independently and their respective outputs are fed into the merge predicate M . Then, M produces the merged result as the output of the parallel composition. Each merge predicate reflects a parallel scheme, therefore the parallel composition is parametric over M , which is indicated by the notation M . Concretely, let P and Q be the parallel processes with respective state variables v 0 and v 1 (which are not necessarily disjoint), then

P M Q = H a SIM ((P X ∧ Q Y ) M ) where P X (Q Y ) makes an X (Y )-version of P (Q) by adding the time variable ti in P (Q) with the X (Y )-subscript, i.e., P X = P (ti = ti X ∧ v 0 = v 0 ) = P[ti X /ti ] Q Y = Q (ti = ti Y ∧ v 1 = v 1 ) = Q[ti Y /ti ] Remark 4. Note that the H a SIM -healthiness of parallel composition P M Q is enforced. Otherwise, H a
SIM -healthiness could be violated, because the merge predicate M can be arbitrary. We could investigate well-defined merge predicates that guarantee H a SIM -healthiness by definition (just as the merge predicate SIM, which does), but it is not the concern in this paper.

For Simulink, we define a new merge predicate:

SIM = ti X = ti Y = ti ∧ v 0 = v 0 ∧ v 1 = v 1
It states that the parallel processes are synchronous on time (ti X = ti Y ), i.e., their termination time should be identical (+∞ for non-termination); and the output values of the shared state variables v 0 ∩ v 1 should keep consistent. We denote the parallel operator defined by SIM as SIM . For brevity, in the remainder, we write for SIM unless otherwise stated. The following property states that is equivalent to conjunction.

Property 5. P Q ≡ P ∧ Q if P and Q are Simulink processes.

Proof. According to the definition,

P Q = H a SIM ((P X ∧ Q Y ) SIM), where (P X ∧ Q Y ) SIM = (P[ti X /ti ] ∧ Q[ti Y /ti ]) (ti X = ti Y = ti ∧ v 0 = v 0 ∧ v 1 = v 1 ) = ∃ti X , ti Y , v 0 , v 1 • P[ti X , v 0 /ti , v 0 ] ∧ Q[ti Y , v 1 /ti , v 1 ] ∧(ti X = ti Y = ti ∧ v 0 = v 0 ∧ v 1 = v 1 ) = P ∧ Q Since P and Q are H a SIM -healthy, P ∧ Q is also H a SIM -healthy (Property 3
). Then, we can get

P Q = H a SIM ((P X ∧ Q Y ) SIM) = H a SIM (P ∧ Q) = P ∧ Q The property is proved.
Although parallel composition is equivalent to conjunction in essence, we distinguish the two concepts in this paper. Concretely, parallel composition between blocks in a Simulink diagram or within a subsystem is called conjunction; while parallel composition between subsystems is called parallel composition. Consider the Simulink diagram in Fig. 1, where each block can be translated to a Simulink process. The semantics of subsystem Plant can be defined by the conjunction Integrator0 ∧ Integrator1, while the semantics of the whole diagram can be defined by the parallel composition Plant Control, which is logically equivalent to Plant ∧ Control.

Syntactic sugar

For brevity in the ensuing presentation, we introduce some syntactic sugar for the HUTP representation of Simulink semantics. Notice that the following notations are different from the definitions in (Xu et al., 2022a).

Let ∼ P denote a predicate relating ∼ v and ∼ v, then ∼ P = H a SIM (∀t ∈ (ti , ti ) • ∼ P ( ∼ v(t), ∼ v(t)))
is a continuous process reflecting the flow of ∼ v over the time interval (ti , ti ) for ti < ti , and it states that ∼ P holds at every instant t from ti to ti . Note that although the input and output state variables v and v do not appear in ∼ P , they are in the alphabet of ∼ P , or in other words, v and v can take arbitrary values. We can also bind v and v to the initial and final values of ∼ v, respectively, resulting in the following definitions:

∼ P = v = ∼ v(ti ) ∧ ∼ P ∼ P = ∼ P ∧ v = ∼ v(ti -) ∼ P = v = ∼ v(ti ) ∧ ∼ P ∧ v = ∼ v(ti -)
Especially, we define

Idle = ∼ v = 0
Besides, we add subscripts to the above definitions to constrain the duration. For example,

∼ P d = ∼ P ∧ ti -ti = d ∼ P ≤d = ∼ P ∧ ti -ti ≤ d
Note that the above continuous processes are all Simulink processes as they are H a SIM -healthy. A causal sequence of operations or events which is assumed to take no time is called super-dense computation [START_REF] Manna | Verifying hybrid systems[END_REF]. Under superdense computation, rendering the time to compute the discrete operations is negligible. However, the causal order of computations is still significant. Under the assumption of super-dense computation, a discrete process is defined by

[P ] = ti = ti < +∞ ∧ P where P denotes a predicate relating v and v . It executes instantly at time ti = ti , rather than continuously over a time interval. Note that [P ] is not a Simulink process as its duration is 0. This would violate the healthiness condition H SIM . However, the sequential composition of [P ] and a Simulink process is usually H a SIM -healthy, as demonstrated in the later content. We define

Skip = ti = ti < +∞ ∧ v = v
Similar to Property 16 in (Xu et al., 2022a), it can be proved that (Skip P) = (P Skip) = P for any Simulink process P.

Since Simulink processes form a complete lattice according to the discussion at the end of Section 2.3.1, recursion can be defined. Theoretically, recursion is denoted by the fixed points of the equation X = F (X), where F constructs the body of the recursion. If F is monotonic, the fixed points of X = F (X) also form a complete lattice by the Knaster-Tarski theorem [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF]. The least fixed point is denoted by µX.F (X), based on which we can define

P * = µX.(Skip ∨ P X)
where P is a Simulink process.

Semantics for Simulink blocks

In this section, we give the HUTP semantics of Simulink blocks in terms of Simulink processes. A (non-hierarchical) Simulink diagram consists of blocks graphically connected by directed lines. Each such connection is the output signal of a unique block. We represent a signal by a variable x defined as a real-valued function of time x ∈ F = R ≥0 → R. A Simulink block can be represented by the tuple (I, O, S, R), where I is the set of input variables, O is the set of output variables, S is the set of internal state variables, and R is a relation between the signals F I , F S and F O . In the following, we use x(t) for the vector of input variables as a function of time, y(t) for the vector of output variables, and s(t) for the vector of state variables. Note that s is different from the state variables v in HUTP (Section 2.3), and the latter is actually the group of x, s and y.

Example 6. A continuous Add block specifies that the output signal y is the sum of the two input signals x 0 and x 1 . Here I = {x 1 , x 2 }, O = {y}, S = ∅, and the relation for R is given by

∀t ≥ 0 • y(t) = x 1 (t) + x 2 (t).
Example 7. A discrete Add block with sample time st > 0 specifies that the output is updated to the sum of inputs whenever the time is a multiple of st, and keeps constant otherwise. Here, I, O and S are the same as before. The relation for R is given by

∀k ∈ N • ∀t ∈ [k • st, (k + 1)st) • y(t) = x 1 (k • st) + x 2 (k • st).
Example 8. A continuous Switch block with condition ">0" specifies that the output y is equal to the top input x 1 if the middle input x 2 satisfies the condition; and the bottom input x 3 otherwise (x 2 ≤ 0).

Here I = {x 1 , x 2 , x 3 }, O = {y} and S = ∅. The relation for R is given by ∀t ≥ 0 • y(t) = x 1 (t) x 2 (t) > 0 y(t) = x 3 (t).
∀k ∈ N • ∀t ∈ [k • st, (k + 1)st) • s(t) = x(k • st) ∧ ∀t ∈ [0, st) • y(t) = v 0 ∧ ∀k ∈ N • ∀t ∈ [(k + 1)st, (k + 2)st) • y(t) = s(k • st).
Example 10. An Integrator block with initial state s 0 specifies that its state is the integral of the input signal and the output signal is consistent with the state. Here I = {x}, O = {y} and S = {s}. The relation for R is given by R(b i ) be the sets of input variables, output variables, state variables, and relation for block b i , respectively. We require the state variables S(b i ) are disjoint from each other and from the input/output variables. Let {v j } 1≤j≤ be the set of variables denoting the lines (signals) connecting blocks of the Simulink diagram. Each v j is in at most one O(b i ). The semantics of the Simulink diagram is a relation on v i (t), defined to be the conjunction of the relation for each block:

y(0) = s(0) = s 0 ∧ ∀t > 0 • ṡ(t + ) = x(t) ∧ s(t -) = s(t) = y(t).

Given a Simulink diagram consisting of blocks {b

i } 1≤i≤m . Let I(b i ), O(b i ), S(b i ) and
R = 1≤i≤m R(b i )
Following the above analysis, we can define the HUTP semantics for (nonhierarchical) Simulink diagrams. The definition is bottom-up as we start from the individual blocks, then combine them to form the semantics of the entire diagram.

Discrete blocks

A discrete block is specified by a sample time st > 0, initial state s 0 , and two functions f and g for updating the state and computing the output, respectively. The values of state and output variables of a discrete block are constant on each time interval [k •st, (k +1)st) for k ∈ N. Hence, we only need to specify their values at times k • st. They satisfy the following equations:

s(k • st) = f (x(k • st), s((k -1) • st)) y(k • st) = g(x(k • st), s((k -1) • st))
where we take s((k -1)st) to be s 0 for k = 0. The main idea here is that the output and state at the current round is computed from the input at current round and state at previous round.

For example, the discrete Add block in Example 7 is given by

y(k • st) = g(x 1 (k • st), x 2 (k • st)) = x 1 (k • st) + x 2 (k • st).
There is no need for f as there are no state variables. The discrete Unit Delay block in Example 9 is given by

s(k • st) = f (x(k • st), s((k -1) • st)) = x(k • st) y(k • st) = g(x(k • st), s((k -1) • st)) = s((k -1) • st).
Now we describe how to encode the above formulas using the HUTP language. A discrete block can either be stateful or stateless. For a stateless discrete block, there is no need for the function f . The computation of g is instant and can be expressed by the following discrete process:

Comp = [y = g(x )].
Intuitively, this means that the output y is computed from the input values only after they are computed by other processes at the same round, that is after the values of x are all available. This will enforce the ordering between computation of different blocks, as we will demonstrate afterwards.

After the computation, the block will keep quiescent for the period of st (sample time), i.e., the output y remains unchanged, specified by the following continuous process: The state variables s and output variables y are updated periodically according to functions f and g, respectively. The update is instant and can be described by the following discrete process:

Period = ∼ y = 0 st
Comp = [s = f (x , s) ∧ y = g(x , s)]
The waiting period of the stateful discrete block is represented by the following continuous process:

Period = ∼ s = ∼ y = 0 st
During the period, state variables s and output variables y keep unchanged. Thus, similar to DisBlock, the hybrid process of the stateful discrete block is given by

DisBlockSt = Init (Comp Period ) * Comp Tail where Tail = ∼ s = ∼ y = 0 ≤st
Theorem 11. DisBlock and DisBlockSt are Simulink processes.

Proof. The sequential composition Comp Period can be expanded to

[y = g(x )] ∼ y = 0 st = ∼ y(ti ) = g( ∼ x(ti )) ∧ ∼ y = 0 st
which is H a SIM -healthy according to the definition in Section 3.3. Similarly, we can prove Comp Tail is also H a SIM -healthy. According to Property 3 and by induction on the number of iterations of * , DisBlock is H a SIM -healthy. Similarly, we can also prove DisBlockSt is H a SIM -healthy.

Example 12. Consider two discrete blocks in sequence. One block B 1 has input line x and output line y, and set y := x + 1 every sample time 1; the other block B 2 has input line y and output line z, and set z := 2 • y every sample time 1. The Simulink processes for B 1 and B 2 are given by:

B 1 HUTP = ([y = x + 1] ∼ y = 0 1 ) * [y = x + 1] ∼ y = 0 ≤1 B 2 HUTP = ([z = 2 • y ] ∼ z = 0 1 ) * [z = 2 • y ] ∼ z = 0 ≤1
We first rewrite the above two definitions to corresponding logical equations.

By the definition of sequential composition , the definition for

[y = x + 1] ∼ y = 0 1 in B 1 HUTP expands to [y = x + 1] ∼ y = 0 1 (1) = (ti = ti < +∞ ∧ y = x + 1) (2)    ti < ti < +∞ ∧ x = ∼ x(ti ) ∧ y = ∼ y(ti ) ∧∀t ∈ (ti , ti ) • ∼ y(t) = 0 ∧ ti -ti = 1 ∧RC ( ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ x, ∼ y, ti , ti )    (3) = ∃t 0 , x 0 , y 0 • ti = ti 0 < +∞ ∧ y 0 = x 0 + 1 ∧ti 0 < ti < +∞ ∧ x 0 = ∼ x(ti 0 ) ∧ y 0 = ∼ y(ti 0 ) ∧∀t ∈ (ti 0 , ti ) • ∼ y(t) = 0 ∧ ti -ti 0 = 1 ∧RC ( ∼ x, ∼ y, ti 0 , ti ) ∧ SD( ∼ x, ∼ y, ti 0 , ti ) = ti -ti = 1 ∧ ∼ y(ti ) = ∼ x(ti ) + 1 ∧ ∀t ∈ (ti , ti + 1) • ∼ y(t) = 0 ∧RC ( ∼ x, ∼ y, ti , ti + 1) ∧ SD( ∼ x, ∼ y, ti , ti + 1)
Note that although ∼

x does not appear in ∼ y = 0 1 , it is in the alphabet of B 1 HUTP . Therefore, we cannot remove x = ∼ x(ti ) from ∼ y = 0 1 (see (3)). Besides, by H a 4 , the continuous state variables in ∼ y = 0 1 are right continuous and semi-differentiable during the period, specified by RC and SD. Then, by induction, we can get

([y = x + 1] ∼ y = 0 1 ) * = Skip ∨      ∃n ∈ N + • ti -ti = n ∧∀k ∈ N <n • ∼ y(ti + k) = ∼ x(ti + k) + 1 ∧∀t ∈ (ti + k, ti + k + 1) • ∼ y(t) = 0 ∧RC ( ∼ x, ∼ y, ti , ti + n) ∧ SD( ∼ x, ∼ y, ti , ti + n)      (4)
where N + = N\{0} and N <n = {k ∈ N | k < n}. Similar to (1),

[y = x + 1] ∼ y = 0 ≤1 = 0 < ti -ti ≤ 1 ∧ ∼ y(ti ) = ∼ x(ti ) + 1 ∧∀t ∈ (ti , ti ) • ∼ y(t) = 0 ∧RC ( ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ x, ∼ y, ti , ti )
Based on the above results, B 1 HUTP expands to

∃n ∈ N • n < ti -ti ≤ n + 1∧ ∀k ∈ N <n • ∼ y(ti + k) = ∼ x(ti + k) + 1 ∧ ∼ y(ti + n) = ∼ x(ti + n) + 1 ∧∀t ∈ (ti + k, ti + k + 1) • ∼ y(t) = 0 ∧ ∀t ∈ (ti + n, ti ) • ∼ y(t) = 0 ∧RC ( ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ x, ∼ y, ti , ti ) Similarly, B 2 HUTP expands to ∃n ∈ N • n < ti -ti ≤ n + 1∧ ∀k ∈ N <n • ∼ z(ti + k) = 2 • ∼ y(ti + k) ∧ ∼ z(ti + n) = 2 • ∼ y(ti + n) ∧∀t ∈ (ti + k, ti + k + 1) • ∼ z(t) = 0 ∧ ∀t ∈ (ti + n, ti ) • ∼ z(t) = 0 ∧RC ( ∼ y, ∼ z, ti , ti ) ∧ SD( ∼ y, ∼ z, ti , ti )
The connection of B 1 and B 2 can be defined by

B 1 HUTP ∧ B 2 HUTP , i.e., ∃n ∈ N • n < ti -ti ≤ n + 1∧ ∀k ∈ N <n • ∼ y(ti + k) = ∼ x(ti + k) + 1 ∧ ∼ z(ti + k) = 2 • ∼ y(ti + k) ∧ ∼ y(ti + n) = ∼ x(ti + n) + 1 ∧ ∼ z(ti + n) = 2 • ∼ y(ti + n) ∧∀t ∈ (ti + k, ti + k + 1) • ∼ y(t) = ∼ z(t) = 0 ∧∀t ∈ (ti + n, ti ) • ∼ y(t) = ∼ z(t) = 0 ∧RC ( ∼ x, ∼ y, ∼ z, ti , ti ) ∧ SD( ∼ x, ∼ y, ∼ z, ti , ti )
This example demonstrates that the parallel composition of the HUTP semantics for B 1 and B 2 simplifies to the desired form, enforcing that the computation in B 1 is performed before that of B 2 at every sample time. We further note that the values of

Continuous blocks

We consider two kinds of continuous blocks: computation blocks and Integrator blocks. A computation block is a stateless block with sample time 0 (see Examples 6 and 8). When building Simulink diagrams, the sample time of computation blocks are usually inherited from integrator blocks by sample time propagation. It is specified by a function g from its input x to its output y, so its relation is specified by ∀t ≥ 0 • y(t) = g(x(t)). Hence, its HUTP representation is

ConBlock = ∼ y = g( ∼ x)
Remark 13. For a continuous block, our concern is the evolution of its output signals ( ∼ y) according to its input signals ( ∼ x) rather than its initial and/or final observations (x, y, x , and y ). Thus, we use • rather than

• in ConBlock.

The Integrator block is already given in Example 10, and its HUTP representation is given by

IntBlock = ∼ y(ti ) = ∼ s(ti ) = s 0 ∧ ∼ s + = ∼ x ∧ ∼ s -= ∼ s = ∼ y
where s 0 is the initial state of s, and ∼ s + and ∼ s -denote the right-hand derivative and the left limit of

P ∧ ∼ Q = ∼ P ∧ ∼ Q Proof. According to the definition of • , ∼ P ∧ ∼ Q = 0 < ti < ti < +∞ ∧ ∀t ∈ (ti , ti ) • ∼ P ( ∼ v(t), ∼ v(t)) ∧RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti )∧ 0 < ti < ti < +∞ ∧ ∀t ∈ (ti , ti ) • ∼ Q( ∼ v(t), ∼ v(t)) ∧RC ( ∼ v, ti , ti ) ∧ SD( ∼ v, ti , ti ) = ∼ P ∧ ∼ Q
The property is proved.

Example 16. Consider an Integrator block B 3 with state s, input line z and output line x, and s is set to 0 initially. The Simulink process for B 3 is given by:

B 3 HUTP = ∼ x(ti ) = ∼ s(ti ) = 0 ∧ ∼ s + = ∼ z ∧ ∼ s -= ∼ s = ∼ x =   ti < ti < +∞ ∧ ∼ x(ti ) = ∼ s(ti ) = 0 ∧∀t ∈ (ti , ti ) • ∼ s(t + ) = ∼ z(t) ∧ ∼ s(t -) = ∼ s(t) = ∼ x(t) ∧RC ( ∼ x, ∼ s, ∼ z, ti , ti ) ∧ SD( ∼ x, ∼ s, ∼ z, ti , ti )  

Composition

A (non-hierarchical) Simulink diagram is composed of discrete and continuous blocks connected by lines. Given such a diagram, we can construct a directed graph G, called its causality graph, as follows. The vertices of G are the input/output variables, and there is an edge from v i to v j if v i is the input and v j is the output of some non-delay discrete or computation block B k . Note that the discrete delay block and the integrator block are excluded. If G is acyclic, then the diagram is said to be well-formed. Otherwise, there exist some loops among discrete and/or computation blocks called algebraic loops (also called logical loops in (Zou et al., 2013b)), which may not always admit a solution. Actually, the cycle-freedom of causality graphs is a necessary condition for Simulink diagrams to behave well. In particular, it allows to avoid straightforward deadlocks. To our knowledge, should the causality graph of a diagram contain a cycle, the tool Matlab/Simulink would reject it, returning an error or a warning. Accordingly, we only consider Simulink diagrams with acyclic causality graphs in this paper.

If the diagram is well-formed, its HUTP semantics can be described by the parallel composition of the atomic blocks it contains. Specifically, given a well-formed diagram consisting of n blocks whose semantics are represented by P i (1 ≤ i ≤ n), the semantics of the diagram is denoted by the following parallel composition, which is equivalent to the conjunction by Property 5:

P 1 • • • P n ≡ n i=1 P i
We say the semantics of a diagram is determined if, given any choice of input signals to the overall diagram, there are unique functions for all output and state variables that satisfies n i=1 P i . We wish to prove that under additional conditions related to the unique solvability of ODEs, the HUTP semantics of a well-formed diagram is determined. Before proving this result, we prove the following lemmas.

Lemma 17. Consider a well-formed Simulink diagram consisting of n discrete blocks whose semantics are represented respectively by P i . Given any choice of input signals to the overall diagram, there are unique functions for all input, output, and state variables that satisfy n i=1 P i . Moreover, let st be the sample time of the diagram (greatest common divisor of the sample times of the blocks), then the values of output and state variables depend only on the values of input variables at multiples of st, and they are constant over each time interval [k • st, (k + 1) • st).

Proof. Since the causality graph G of the Simulink diagram is acyclic, we can choose a topological ordering

∼ v 1 , • • •, ∼ v m
for the input and output variables of the blocks in the diagram. For brevity, we assume that the sample time of the diagram is 1. We prove by induction on k that there exist unique values for input, output and state variables on each time interval [k, k + 1). First, consider the base case k = 0, we perform a second induction on the index i in the ordering ∼ v i . For the variable ∼ v i , by the induction hypothesis, we can assume ∼ v j (0) is uniquely determined for each j < i. ∼ v i is either an input to the overall diagram, or the output of some block B j . If B j is a delay block, then ∼ v i (0) is given by the initial value of the state. Otherwise, according to the definition of G, all input variables of the block occur earlier in the topological order, whose values at 0 are uniquely determined by induction, so again ∼ v i (0) is uniquely determined. Since the values of state variables at time 0 is a function of input variables at time 0 and the initial state, they are also determined. Now consider the inductive case k + 1. Again, we induct on the index i in the ordering

∼ v i . If ∼ v i is
an input to the overall diagram, then it is already determined. So suppose ∼ v i is the output of some block B j . If the sample time of block B j is a multiple of k + 1, again we divide into cases for delay block and non-delay block. For the delay block, the value of ∼ v i (k + 1) is given by the value of state at a previous time. For non-delay blocks, the value of

∼ v i (k + 1) is a function of ∼ v j (k + 1)
for j < i and state variables at time k. In both cases the value is determined. Finally, if the sample time of B j is not a multiple of k + 1, we have

∼ v i (k + 1) = ∼ v i (k). This shows ∼ v i (k + 1) is determined for all 1 ≤ i ≤ m.
Then, since the state variables at time k + 1 is a function of variables ∼ v i (k + 1) and state variables at time k, they are determined as well.

In this way, we construct the values of all ∼ v i , as well as that of the state variables, at the integer time points. In the process, we have considered relations for all blocks. Hence, the solution we obtained satisfies the relation n i=1 P i . Finally, by the construction in this proof, it is clear that the output and state variables depend only on the values of input variables at each integer k, and are constant over each time interval [k, k + 1).

Lemma 18. For a well-formed Simulink diagram consisting of continuous blocks, let v be the line variables of the diagram, where x denote the input variables to the diagram and s and y represent the state and output variables of the Integrator blocks in the diagram. Then, (1) its semantics can be expressed in the form of where

y(ti ) = s(ti ) = s 0 ∧ ∼ P ( ∼ v) ∧ ∼ s + = E( ∼ x ∼ s) ∧ ∼ s -= ∼ s = ∼ y (
Init = m i=1 ∼ y i (ti ) = ∼ s i (ti ) = s i,0 Evolve = m i=1 ∼ s + i = ∼ a i ∧ ∼ s - i = ∼ s i = ∼ y i ∧ m+n j=m+1 ∼ c j = g j ( ∼ b j )
where s i,0 is the initial value of s i . For each computation block B j , it defines a variable substitution mapping Γ jk . Concretely, it maps each output variable c jk ∈ c j of the block to an expression g jk on the input variables b j , i.e., Γ jk (c jk ) = g jk (b j ), where all the g jk form the function g j . Since the diagram is well-formed, the input and output variables of all computation blocks in the diagram form a directed acyclic graph. Therefore, all the mapping functions Γ jk can be composed to form a function Γ that maps the input variable a i (which could be some c j,k ) of each Integrator block B i to Γ(a i ) which is an expression on x s, denoted e i (x s). Note that for a i / ∈ dom(Γ), we let Γ(a i ) = a i . All the expressions e i (x s) form the expression function E. Besides, m+n j=m+1 ∼ c j = g j ( ∼ b j ) denotes the relation ∼ P in the representation. In summary, the formula of ( 6) can be expresses in the form of ( 5).

(2) According to Equation ( 5), the right-hand derivative of

             ∼ x(ti ) = ∼ s(ti ) = 0∧ ∃n ∈ N • n < ti -ti ≤ n + 1 ∧ ∀k ∈ N <n • ∼ y(ti + k) = ∼ x(ti + k) + 1 ∧ ∼ z(ti + k) = 2 • ∼ y(ti + k)∧ ∼ y(ti + n) = ∼ x(ti + n) + 1 ∧ ∼ z(ti + n) = 2 • ∼ y(ti + n)∧ ∀t ∈ (ti + k, ti + k + 1) • ∼ y(t) = ∼ z(t) = 0 ∧ ∼ s(t) = ∼ z(t)∧ ∀t ∈ (ti + n, ti ) • ∼ y(t) = ∼ z(t) = 0 ∧ ∼ s(t) = ∼ z(t)∧ ∀t ∈ (ti , ti ) • ∼ s(t -) = ∼ s(t) = ∼ x(t)∧ RC ( ∼ x, ∼ y, ∼ z, ∼ s, ti , ti ) ∧ SD( ∼ x, ∼ y, ∼ z, ∼ s, ti , ti )              Since ∼
z is differentiable within the intervals (ti +k, ti +k +1) and (ti +n, ti ), ∼ s(t + ) is replaced with ∼ s(t) in the above formula. For ensuring the continuity of ∼ s, there should be ∼ s -= ∼ s during the period. For the above formula, we get the following unique solution:

∀t ∈ [ti , ti ) • ∃d ∈ R • d = t -ti ∧     ∼ s(t) = 2 • 3 d (d -d ) + 3 d -1 ∼ x(t) = 2 • 3 d (d -d ) + 3 d -1 ∼ y(t) = 3 d ∼ z(t) = 2 • 3 d    
which is exactly the semantics of the Simulink diagram (here • : R → Z is the floor function).

Hierarchical Simulink diagrams

Modular design is a design principle that subdivides a system into smaller parts called modules (or subsystems), which can be independently created, modified, replaced, or exchanged with other modules or between different systems. The modelling of hierarchical Simulink diagrams reflects the principle of modular design: a Simulink diagram is composed of hierarchical subsystems, which may include enabled or triggered behaviours. In this section, we establish the HUTP semantics for normal, triggered and enabled subsystems, which forms hierarchical Simulink diagrams.

Normal subsystems

A normal subsystem groups a set of atomic Simulink blocks together, and will execute them as a single unit. Simulink distinguishes the input (output) variables i (o) as seen from within the subsystem and the input (output) variables ī (ō) as seen from outside (as lines in the overall diagram). For normal subsystems, we will identify the variables i with ī, and variables o with ō (see x and y in Fig. 2). Later on, we may not identify i with ī for triggered and enabled subsystems.

A normal subsystem is well-formed if its causality graph is acyclic. The effect of executing a well-formed normal subsystem is equivalent to executing the corresponding Simulink diagram consisting of the same set of blocks. Therefore, the semantics of a normal subsystem can be defined by the conjunction of the semantics of all the blocks it contains, as specified in Section 4.3. In the translation algorithm from Simulink to HCSP presented in (Zou et al., 2013b), the subsystem is flattened by connecting the in-ports and outports as seen from inside with the corresponding in-ports and out-ports on the outside. The result of this process is shown on the right side of Fig. 2. This flattening makes the translation process easier to implement, and is necessary for collecting together all continuous blocks in the diagram for translation to a single ODE. However, it violates to some extent the principle of modular design, i.e., the hierarchical structure of the Simulink diagram is not reflected in the translated HCSP process. In this paper, subsystems are not flattened and therefore the structure of Simulink diagrams can be reflected in their HUTP semantics. For example, the Simulink diagram on the left of Fig. 2 is composed of two well-formed subsystems Subsystem0 and Subsystem1 whose semantics are given by

Subsystem0 HUTP = Int0 HUTP ∧ Bias0 HUTP Subsystem1 HUTP = Int1 HUTP ∧ Bias1 HUTP
where Bias0 HUTP and Bias1 HUTP are discrete processes (Section 4.1), and Int0 HUTP and Int1 HUTP are continuous processes (Section 4.2).

Triggered subsystems

A triggered subsystem only contains blocks with inherited sample time (-1). Such a block has no specified sample time, whose execution depends solely on the triggering signal. Concretely, the blocks execute at the instant when the trigger condition on the trigger line holds. A sketch of a triggered subsystem with rising edge trigger is shown in Fig. 3. Similar to well-formed normal subsystems, a triggered subsystem is well-formed if its causality graph is acyclic. The trigger port senses the input signal z in real time. In this paper, we assume that each triggered subsystem has only one trigger line. There are three basic trigger types: rising, falling and either. For the rising edge trigger, the subsystem is triggered at time t whenever (1) z rises from negative to non-negative at t or (2) z rises from non-positive to positive at t. Formally,

∼ z(t -) < 0 ∧ ∼ z(t) ≥ 0 ∨ ∼ z(t -) ≤ 0 ∧ ∼ z(t) > 0
The triggering conditions for the other two trigger types can be defined similarly. Therefore, in this section, we only define the HUTP semantics for triggered subsystems with rising edge trigger. In this paper, we assume that the trigger line of each triggered subsystem is the output of a discrete block, hence piecewise constant with some sample time st. Treatment of continuous triggering will be more complicated, involving analysis of zero-crossing detection and potential cascade of zero-crossings [START_REF] Benveniste | Non-standard semantics of hybrid systems modelers[END_REF].

Trigger Blocks

Fig. 3: A sketch of a triggered subsystem with rising edge trigger Now we consider the HUTP semantics of well-formed triggered subsystems. The subsystem is triggered at current time iff (1) the previous value of the signal z is less than 0 and the current value of z reaches or crosses 0; or (2) the previous value of z is not greater than 0 and the current value of z crosses 0. After that, the signal z will keep "not triggering" for some period until it satisfies the trigger condition again. Therefore, the behaviour of z between two adjacent triggering time instants can be defined by

Trigger = [z < 0 ∧ z ≥ 0 ∨ z ≤ 0 ∧ z > 0] ¬trigger where trigger = z -< 0 ∧ z ≥ 0 ∨ z -≤ 0 ∧ z > 0
When triggered, the subsystem gets the latest values from the input ports, given by the relation ∼ x(ti ) = ∼ a(ti ), where ti is the current triggering time, x denote the input variables from within the subsystem while a denote the input variables to the overall subsystem (see Fig. 3). The reason we distinguish x and a is that their values are not the same at all times: during the idle period of the subsystem, x will keep unchanged while a can change dynamically according to the behaviour of its source subsystem. The input variables x synchronise with the input variables a from the outside only when the triggering signal arrives. However, for output variables, it is not necessary to distinguish the output variables to within the subsystem and the output variables from the overall subsystem, because the output variables are controlled by the subsystem solely and they will not be modified by other subsystems, i.e., they always keep consistent.

After the input synchronisation (x obtain the values of a), the subsystem will perform the computation and then keep idle for some period, which can be represented by the conjunction of the idle process ∼ v = 0 , where v are the variables inner the subsystem, and the continuous processes

∼ P i (1 ≤ i ≤ n)
of all blocks in the subsystem. Therefore, according to Property 15, which indicates

∼ v = 0 ∧ n i=1 ∼ P i = ∼ v = 0 ∧ n i=1 ∼ P i Trigger Bias Gain
Fig. 4: An example of a triggered subsystem with rising edge trigger the behaviour of the subsystem can be captured by

SubSys = ∼ x(ti ) = ∼ a(ti ) ∧ ∼ v = 0 ∧ n i=1 ∼ P i
Before triggering, the variables v of the lines in the subsystem should be initialised, because if the subsystem is not triggered at the beginning, it should be guaranteed that the values of v are valid. By default, v are initialised to 0 in Simulink. If the subsystem is not triggered initially, the values of v will keep constant. Besides, the trigger line z should also be initialised, because at the beginning, it will compare the initial value of z with the current value of z to determine if the subsystem should be triggered at the time. By default, we also set z to 0 initially. Then, the initialisation is specified by

InitTrig = [v = 0 ∧ z = 0] (Trigger ∧ SubSys ∨ Idle)
In summary, the semantics of triggered subsystem can be defined by

TrigSubSys = InitTrig (Trigger ∧ SubSys) *
When creating the causality graph of a triggered subsystem, we add edges from the trigger line to each input line inside the subsystem, since whether the input lines receive values from the outside is determined by the trigger line. For the example in Fig. 4, the causality graph G is given by {(z, x), (a, x), (x, y), (y, b)}.

Example 21. Consider the triggered subsystem in Fig. 4, we only analyse SubSys. Concretely, SubSys is equivalent to

∼ x(ti ) = ∼ a(ti ) ∧ ∼ x = ∼ y = ∼ b = 0 ∧ ∼ b = 2 • ∼ y ∧ ∼ y = ∼ x + 1
which can expand as follows:

∼ x(ti + ) = ∼ x(ti ) = ∼ a(ti ) = ∼ a(ti + ) ∧ ∼ y(ti ) = ∼ y(ti + ) ∧ ∼ b(ti ) = ∼ b(ti + ) ∧ (7) ∀t ∈ (ti , ti ) • ∼ x(t) = ∼ y(t) = ∼ b(t) = 0 ∧ ∼ b(t) = 2 • ∼ y(t) ∧ ∼ y(t) = ∼ x(t) + 1 (8) ∧RC ( ∼ a, ti , ti ) ∧ SD( ∼ a, ti , ti )
This process specifies the behaviour that the subsystem is triggered at the beginning and then keeps idle for some period. First, the subsystem gets the latest input at ti, i.e.,

∼

x(ti ) = ∼ a(ti ); then, according to (8), we can get the relation

∼ b(ti + ) = 2 • ∼ y(ti + ) ∧ ∼ y(ti + ) = ∼ x(ti + ) + 1; combining (7), we can infer that ∼ b(ti ) = 2 • ∼ y(ti ) ∧ ∼ y(ti ) = ∼ x(ti ) + 1 (9)
which indicates the subsystem executes the computation at the beginning when triggered; afterwards, x, y and b keep constant from ti to ti , and therefore the relation between these variables always holds during the period (see ( 8)).

Theorem 22. If the triggered subsystem is well-formed, then TrigSubSys is a Simulink process with determined semantics.

Proof. According to Property 3 and by induction on the number of iterations of * , TrigSubSys is a Simulink process. When the triggering signal z is determined, the triggering times are determined as well. When triggered, the subsystem gets the latest inputs and performs the execution expressed by a relation between the variables at the time (see ( 9)). Since the subsystem is well-formed, the solution of the relation is unique given any choice of input signals. The signals then keep constant during the period until the next trigger time arrives. Therefore, the semantics represented by TrigSubSys is determined.

Enabled subsystems

An enabled subsystem is similar to a normal subsystem except that its execution depends on the enabled signal: it executes as usual when the value of the enabled signal is larger than 0 and keeps idle otherwise. A sketch of an enabled subsystem is illustrated in Fig. 5. Similar to triggered subsystems, we assume that each enabled subsystem has only one enabling line z. The evolution of the enabled signal z can be seen as an interleaving of positive and non-positive phases. Concretely, the evolution of z can be defined by

(z ≤ 0 ∧ ∼ z > 0 ∨ z ≥ 0 ∧ ∼ z ≤ 0 ) *
In the beginning of a positive phase, it checks if the value of z from the preceding phase (which should be non-positive) is non-positive (z ≤ 0); if so, the value of z will keep positive for some period ( ∼ z > 0 ). The behaviour of non-positive phases are similar.

In a positive phase, the inner input variables x should keep consistent with the input variables a to the overall subsystem, and then the subsystem executes as if it were a normal subsystem. Concretely, let P i (1 ≤ i ≤ n) be the process denoting the semantics of the i-th block in the subsystem, then the behaviour of the enabled subsystem in a positive phase can be described by

Enabled = z ≤ 0 ∧ ∼ z > 0 ∧ ∼ a = ∼ x ∧ n i=1 P i ∧ v = ∼ v(ti -)
where v are the variables of all the lines in the subsystem. Note that a∩v = ∅ and x ⊆ v. In each non-positive phase, the subsystem does nothing and keep idle:

Disabled = z ≥ 0 ∧ ∼ z ≤ 0 ∧ ∼ v = 0
In addition, similar to triggered subsystems, the variables v of the lines in the subsystem should also be initialised. By default, v are initialised to 0. If the subsystem is disabled during the initial period, i.e., z keeps non-positive, then v will keep constant:

Disabled = ∼ z ≤ 0 ∧ ∼ v = 0
Otherwise, i.e., z keeps positive initially, the subsystem is enabled during the period:

Enabled = ∼ z > 0 ∧ n i=1 P i ∧ v = ∼ v(ti -)
In summary, the semantics of an enabled subsystem can be denoted by

EnSubSys = (Enabled ∨ Disabled ) (Enabled ∨ Disabled) *
As with triggered subsystems, when creating the causality graph of an enabled subsystem, we add edges from the enabling line to each input line inside the subsystem. An enabled subsystem is well-formed if its causality graph is acyclic.

Theorem 23. If the enabled subsystem is well-formed, then EnSubSys is a Simulink process with determined semantics.

Proof. According to Property 3 and Theorem 19 and by induction on the number of iterations of * , EnSubSys is a Simulink process. Whether the subsystem is enabled or not depends on the enabling signal z. During the enabled period, the subsystem performs as a (well-formed) normal subsystem with determined semantics; during the disabled period, the subsystem keeps quiescent. In summary, the semantics represented by EnSubSys is determined.

Composite systems

A complex Simulink diagram is usually composed of hierarchical subsystems each encapsulating specific functions. Preferably, the hierarchical structure should be preserved when defining the Simulink semantics. In this section, we show how modular design can be taken into account when defining the HUTP semantics of hierarchical Simulink diagrams.

Overall, we adopt the bottom-up approach for defining the semantics. We start from the normal, enabled and triggered subsystems specified from Sections 5.1 to 5.3. Each well-formed subsystem can be treated as a unit, and we obtain the causality relation between its input and output variables by abstracting from the causality graph of the subsystem. For example, the causality graph of the triggered subsystem in Fig. 4 is {(z, x), (a, x), (x, y), (y, b)}, yielding the causality relation of the subsystem: {(z, b), (a, b)}. The causality graph of a high-level subsystem is then defined in terms of the causality relations of its component subsystems. We say a high-level subsystem is well-formed if (1) all its subsystems are well-formed and (2) the causality graph of the high-level subsystem is acyclic. For a well-formed high-level subsystem, its semantics can be represented by the parallel composition of the subsystems it contains.

Theorem 24. For a well-formed high-level subsystem, if the semantics of its subsystems are determined, then its HUTP semantics is determined and can be represented by a Simulink processes.

Proof. Since the semantics of the subsystems in the high-level subsystem are determined, the theorem can be proved from Theorems 19, 22 and 23 and by the well-formedness of the high-level subsystem (the causality graph of variables constructed from the causality relations of its subsystems is acyclic).

Subsystems on the same level can be connected together by parallel composition. In this way, a Simulink diagram can be organised as a composite system composed of hierarchical subsystems, from atomic (normal, triggered and enabled) subsystems to high-level subsystems.

Example 25. Consider the Simulink diagram on the left of Fig. 2, it is a structured diagram consisting of two well-formed subsystems. Note that although the causality graphs of these two subsystems are {(a, x)} and {(b, y)}, respectively, the causality relations of these two subsystems are empty, as there is no causality relation between x and y. Therefore, this diagram, which is a high-level subsystem, is well-formed. Then, we can define its semantics by the parallel composition of the two subsystems:

Diagram HUTP = Subsystem0 HUTP Subsystem1 HUTP
where Subsystem0 HUTP and Subsystem1 HUTP are referred in Section 5.1.

6. Case study: proving the semantic consistency between Simulink and HCSP

In this section, we illustrate by an example how to prove the semantic consistency between Simulink diagrams and the translated HCSP models based on the simplified HUTP semantics of Simulink. The example is shown in Fig. 2 which is borrowed from Section 6.4 of (Xu et al., 2022a) but with a slight modification. The syntax and semantics of HCSP can be found in [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams (A Deductive Approach[END_REF]. Consider the Simulink diagram in Fig. 2, we set the initial values of variables y and a to 0, then the corresponding HCSP model is shown as follows, by the translation algorithm in (Zou et al., 2013b). In the above process, we use tt to denote the time variable, and it is set to 0 initially. The initial values of a and y, the output lines of two Integrator blocks, are also set to 0. Then, at each iteration, we execute the discrete blocks according to a topological order. In the discrete sub-diagram in Fig. 2 (right), Bias0 is prior to Bias1 as the input of the latter depends on the output of the former. For Bias0, it can execute (update the output x according to the latest input a) if the current time is a multiple of the sample time 2, and it does nothing otherwise, depicted by the HCSP process tt%2 == 0 → x := a + 1. The process of Bias1 is similar. After the discrete blocks update their outputs, the whole diagram waits for 1 time unit which is the greatest common divisor of the sample times of Bias0 and Bias1. During the waiting period, the continuous blocks Int0 and Int1 can evolve. The evolution can be described by an ODE ȧ = y, ẏ = b, ṫt = 1&true 1 skip, which indicates the ODE can only evolve for 1 time unit ( 1 ) and then does nothing (skip). The superscript + means the loop iterates at least once.

We will prove the consistency between the example and the new translated HCSP process (10), by comparing the HUTP semantics of Diagram and Diagram HCSP . The HUTP semantics of HCSP has already been given in (Xu et al., 2022a), but it is based on normal hybrid designs. Since defining the new HUTP semantics of HCSP in terms of abstract hybrid processes is not the concern of this paper, we simply present the definitions which are sufficient to express the HUTP semantics of Diagram HCSP of (10):

• The skip statement terminates immediately having no effect on variables, and it is modelled as the rational identity:

skip HUTP = Skip

• The assignment of the value e to a variable x is modelled as setting

x to e and keeping all other variables constant if e can be successfully evaluated. Let the alphabet be {ti , ti , v, v }, where x ∈ v, then

x := e HUTP = [ϕ(e) ∧ x = e ∧ v \{x } = v\{x}]
where ϕ(e) specifies the condition by which e can be evaluated.

• The sequential composition P; Q behaves as P first and as Q afterwards: • A continuous evolution statement F ( ṡ, s) = 0&B says that the process keeps waiting, and meanwhile keeps continuously evolving following the differential equations F , until the domain constraint B is violated:

P; Q HUTP = P HUTP Q HUTP • The alternative B → P,
F ( ṡ, s) = 0&B HUTP = Exit ∨ (ODE Exit) where Exit = [¬B(s) ∧ s = s] ODE = F ( ṡ, s) = 0 ∧ B[ ∼ s/s] • F ( ṡ, s) = 0&B d P behaves like F ( ṡ, s) = 0&B
, if the evolution terminates before d time units. Otherwise, after d time units of evolution, it moves on to execute P:

F ( ṡ, s) = 0&B d P HUTP = Exit ∨ (ODE <d Exit) ∨(ODE d P HUTP )
where

ODE <d = F ( ṡ, s) = 0 ∧ B[ ∼ s/s] <d ODE d = F ( ṡ, s) = 0 ∧ B[ ∼ s/s] d
The semantics of other statements, like communication (ch?x and ch!e), ODE with communication interruption ( F ( ṡ, s) = 0&B i∈I (io i -→ P i )) and parallel composition (P Q), can also be represented by abstract hybrid processes. Since they are not involved in Diagram HCSP of (10), we will not introduce the details. Note that the above HUTP representations of the HCSP processes are abstract hybrid processes rather than Simulink processes, because skip HUTP and x := e HUTP are not Simulink processes as they violate healthiness condition H SIM .

Hence, the HUTP representation of Diagram HCSP of (10) can expand to

Diagram HCSP HUTP = tt := 0 HUTP a := 0 HUTP y :

= 0 HUTP   tt%2 == 0 → x := a + 1 HUTP tt%3 == 0 → b := x + 1 HUTP ȧ = y, ẏ = b, ṫt = 1&true 1 skip HUTP   + = ∼ a(ti ) = 0 ∧ b = ∼ b(ti ) ∧ x = ∼ x(ti ) ∧ ∼ y(ti ) = 0 ∧ ∼ tt(ti ) = 0 ∧∃n ∈ N + • ti + n = ti ∧ ∀k ∈ N <n • ∼ tt(ti + k) = k∧ ( ∼ x(ti + k) = ∼ a(ti + k) + 1 k%2 = 0 ∼ x(ti + k) = ∼ x(ti + k -1)) ∧ ( ∼ b(ti + k) = ∼ x(ti + k) + 1 k%3 = 0 ∼ b(ti + k) = ∼ b(ti + k -1)) ∧∀t ∈ (ti + k, ti + k + 1) • ∼ a(t) = ∼ y(t) ∧ ∼ y(t) = ∼ b(t) ∧ ∼ tt(t) = 1 ∧ ∼ b(t) = ∼ x(t) = 0 ∧ ∀t ∈ (ti , ti ) • ∼ a(t -) = ∼ a(t) ∧ ∼ y(t -) = ∼ y(t) ∧RC ( ∼ a, ∼ b, ∼ x, ∼ y, ∼ tt, ti , ti ) ∧ SD( ∼ a, ∼ b, ∼ x, ∼ y, ∼ tt, ti , ti )∧ a = ∼ a(ti -) ∧ b = ∼ b(ti -) ∧ x = ∼ x(ti -) ∧ y = ∼ y(ti -) ∧ tt = ∼ tt(ti -)
According to the above result, Diagram HCSP HUTP is H SIM -healthy, i.e., it is a Simulink process. For the HUTP semantics of the left diagram in Fig. 2, we can get Diagram HUTP = Subsystem0 HUTP Subsystem1 HUTP ≡ Subsystem0 HUTP ∧ Subsystem1 HUTP (Property 5) where denotes SIM , and

Subsystem0 HUTP = ∼ a(ti ) = 0 ∧ ∃n ∈ N • 2n < ti -ti ≤ 2(n + 1) ∧∀k ∈ N <n • ∼ x(ti + 2k) = ∼ a(ti + 2k) + 1 ∧ ∼ x(ti + 2n) = ∼ a(ti + 2n) + 1 ∧∀t ∈ (ti + 2k, ti + 2k + 2) • ∼ a(t) = ∼ y(t) ∧ ∼ x(t) = 0 ∧∀t ∈ (ti + 2n, ti ) • ∼ a(t) = ∼ y(t) ∧ ∼ x(t) = 0 ∧∀t ∈ (ti , ti ) • ∼ a(t -) = ∼ a(t) ∧RC ( ∼ a, ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ a, ∼ x, ∼ y, ti , ti ) Subsystem1 HUTP = ∼ y(ti ) = 0 ∧ ∃m ∈ N • 3m < ti -ti ≤ 3(m + 1) ∧∀k ∈ N <m • ∼ b(ti + 3k) = ∼ x(ti + 3k) + 1 ∧ ∼ b(ti + 3m) = ∼ x(ti + 3m) + 1 ∧∀t ∈ (ti + 3k, ti + 3k + 3) • ∼ y(t) = ∼ b(t) ∧ ∼ b(t) = 0 ∧∀t ∈ (ti + 3m, ti ) • ∼ y(t) = ∼ b(t) ∧ ∼ b(t) = 0 ∧∀t ∈ (ti , ti ) • ∼ y(t -) = ∼ y(t) ∧RC ( ∼ b, ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ b, ∼ x, ∼ y, ti , ti )
Note that in the above formulas, for brevity, we omit the state variables and replace them by the corresponding output variables, because the state variable and the output variable of an Integrator block are consistent in this setting.

However

(ti -ti = N ) ∧ Subsystem0 HUTP = (ti -ti = N ) ∧ Int0 HUTP ∧ Bias0 HUTP can expand to ti -ti = N ∧ ∼ a(ti ) = 0 ∧ ∀K ∈ N <N • ∼ x(ti + K) = ∼ a(ti + K) + 1 K%2 = 0 ∼ x(ti + K) = ∼ x(ti + K -1) ∧∀t ∈ (ti + K, ti + K + 1) • ∼ a(t) = ∼ y(t) ∧ ∼ x(t) = 0 ∧∀t ∈ (ti , ti ) • ∼ a(t -) = ∼ a(t) ∧ RC ( ∼ a, ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ a, ∼ x, ∼ y, ti , ti )
We can also reformulate (ti -ti = N ) ∧ Subsystem1 HUTP by shortening the step size from 3 to 1: Comparing with the proof of semantic consistency based on normal hybrid designs in Section 6.4 of (Xu et al., 2022a), the proof in this section is more formal and concise, because we adopt Simulink processes as the semantic foundation for Simulink. After all, Simulink processes, a subset of abstract hybrid processes, are much simpler than normal hybrid designs, and arguably more suitable for defining the Simulink semantics.

ti -ti = N ∧ ∼ y(ti ) = 0 ∧ ∀K ∈ N <N • ∼ b(ti + K) = ∼ x(ti + K) + 1 K%3 = 0 ∼ b(ti + K) = ∼ b(ti + K -1) ∧∀t ∈ (ti + K, ti + K + 1) • ∼ y(t) = ∼ b(t) ∧ ∼ b(t) = 0 ∧∀t ∈ (ti , ti ) • ∼ y(t -) = ∼ y(t) ∧ RC ( ∼ b, ∼ x, ∼ y, ti , ti ) ∧ SD( ∼ b, ∼ x,
) = 0 ∧ ∀K ∈ N <N • ( ∼ x(ti + K) = ∼ a(ti + K) + 1 K%2 = 0 ∼ x(ti + K) = ∼ x(ti + K -1)) ∧ ( ∼ b(ti + K) = ∼ x(ti + K) + 1 K%3 = 0 ∼ b(ti + K) = ∼ b(ti + K -1)) ∧∀t ∈ (ti + K, ti + K + 1) • ∼ a(t) = ∼ y(t) ∧ ∼ y(t) = ∼ b(t) ∧ ∼ b(t) = ∼ x(t) = 0 ∧∀t ∈ (ti , ti ) • ∼ a(t -) = ∼ a(t) ∧ ∼ y(t -

Related works

There is a large amount of existing work on formal semantics of Simulink and translation of Simulink models to other languages as part of various system design workflows. Initial work focused on the discrete part of Simulink. Tripakis et al. described a translation of discrete Simulink to the dataflow language Lustre [START_REF] Tripakis | Translating discretetime Simulink to Lustre[END_REF]. Dragomir et al. translates Simulink's hierarchical block diagrams into an algebra of transformers connected together via series, parallel and feedback operators [START_REF] Dragomir | Compositional semantics and analysis of hierarchical block diagrams[END_REF]. In follow-up work, Preoteasa et al. proved the determinacy of these translations, showing that the semantics of the resulting model does not depend on the various choices made during translation [START_REF] Preoteasa | Mechanically proving determinacy of hierarchical block diagram translations[END_REF]. The proofs are formalised in the interactive theorem prover Isabelle/HOL. These work resulted in the Refinement Calculus of Reactive Systems (RCRS) toolset for modelling and reasoning about reactive systems [START_REF] Dragomir | The refinement calculus of reactive systems toolset[END_REF]. Compared to RCRS, we consider in addition the continuous blocks in Simulink (without discretisation), triggered and enabled subsystems, and multi-rate systems, establishing the determinacy of the semantics in this more general setting. Ye et al. present a compositional assume-guarantee reasoning framework to provide a purely relational mathematical semantics for discrete time Simulink diagrams, and then to verify the diagrams against the contracts in the same semantics in UTP [START_REF] Ye | Compositional assume-guarantee reasoning of control law diagrams using UTP[END_REF]. However, the work only captures single sampling rate Simulink models, while multi-rate models are not supported by the reasoning framework.

Existing work take different approaches to formalise the semantics of continuous blocks in Simulink. Some focused on describing in detail how ODE solving and zero-crossing detection are performed. For example, Bouissou et al. gave an operational semantics for both continous-time and discretetime blocks in Simulink that emphasises the details of numerical simulation [START_REF] Bouissou | An operational semantics for simulink's simulation engine[END_REF]. Other works focused on first giving a mathematically precise definition of the semantics, and then possibly consider connections to numerical simulation results. [START_REF] Lee | Operational semantics of hybrid systems[END_REF] detailed the issues that arise when defining semantics of hybrid systems. They described a semantic model where each signal is given by a function from tags to states, where each tag consists of a time and an integer, thus able to describe multiple computation steps at a single time point. While they give semantics for HyVisual (part of the Ptolemy framework), many of the ideas apply to Simulink as well. Benveniste et al. [START_REF] Benveniste | Contracts for system design[END_REF] gave an alternative semantic model based on the theory of nonstandard analysis, which is able to handle cascades of zero-crossings resulting continuous triggers in the system. Based on this model, Bourke et al. proposed Zélus (Bourke and Pouzet, 2013), extending a Lustre-like synchronous language with ODEs. The Zélus language is then used to give semantics to a large collection of Simulink blocks [START_REF] Bourke | A synchronous look at the Simulink standard library[END_REF]. Compared to semantics based on tags and non-standard analysis, we use a simpler semantic model based on functions from real numbers. On the other hand we currently do not consider continuous triggers and hence cascaded zero-crossings.

Several existing work connected translation from Simulink to models of hybrid systems with verification using either model checking or theorem proving. Librenz et al. [START_REF] Liebrenz | Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X[END_REF] proposed a translation from Simulink diagrams to differential dynamic logic [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF], for verification in the KeYmaera X tool. The work of Agrawal et al. [START_REF] Agrawal | Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations[END_REF] provides a characterisation of Simulink as a translation or interpretation as hybrid automata. [START_REF] Minopoli | SL2SX translator: From Simulink to SpaceEx models[END_REF] translates Simulink into SpaceEx models. Our work originated from the initial translation method of Zou et al. (Zou et al., 2013b) from Simulink models into HCSP, within the MARS platform for analysis, verification and simulation of hybrid systems [START_REF] Chen | MARS: A toolchain for modelling, analysis and verification of hybrid systems[END_REF], and the theory of higher-order UTP (Xu et al., 2022a). We then proposed a unified graphical co-modelling, analysis and verification of CPSs by combining AADL and Simulink/Stateflow (Xu et al., 2022b) based on these works. Compared to these previous works, our method yields simpler translated results, and permits easier proofs of semantic determinacy as well as correctness of translation.

Conclusions and future works

Reflecting the complexity of cyber-physical systems design, the semantics of Simulink models is highly complex. In the aim of breaking down this complexity, we abstract the meaning of hierarchical Simulink diagrams into logically and mathematically comprehensible terms, by employing a notion of Simulink processes, a subset of abstract hybrid processes, defined in HUTP. Based on our HUTP semantics of Simulink, we construct a framework for proving Simulink diagrams consistent with their translation into HCSP. We provide a case study that illustrates and justifies this translation.

Future works. As mentioned in Section 5.1, existing translation procedures from Simulink to HCSP begin by flattening some subsystems, which undermines the modular design of Simulink diagrams. Therefore, we will consider improving the translation algorithm to take modular design into account. In this paper, we only introduce parts of the new HUTP semantics of HCSP when proving the semantic consistency in Section 6. In the future, we will provide the complete definition of the new HUTP representation of HCSP, covering communication and ODE with communication interrupts, and prove its consistency with the operational semantics of HCSP. Finally, based on the HUTP representation, we will provide a systematic proof (not just by examples) for the correctness of the translation algorithm from Simulink to HCSP.

Fig. 1 :

 1 Fig. 1: A Simulink diagram of a plant-control model

∼v

  : [ti , ti ) → D stands for its dynamic trajectory from the start time ti to the end time ti , and ∼ v : (ti , ti ) D is a partial function denoting the derivative of ∼ v.

  Example 9. A Unit Delay block with sample time st > 0 and initial value v 0 updates its state whenever the time is a multiple of st, and outputs the previous value of state. Here I = {x}, O = {y} and S = {s}. The relation for R is given by

  ∼ s, respectively. Since ∼ x could be discontinuous but at least right continuous as stated by H 4 , we use ∼ s + rather than ∼ s in the representation. Besides, ∼ s should be continuous and the output signal should keep consistent with the state, so we need the condition ∼ ConBlock and IntBlock are Simulink processes. Proof. ConBlock and IntBlock are H a SIM -healthy by the definition of • specified in Section 3.3. Property 15.

∼

s

  is piecewise differentiable. By induction on the time intervals where ∼ s is differentiable, and using the fact that E satisfies the global Lipschitz condition, we obtain the existence and uniqueness of the solution.The lemma is proved. Theorem 19. For a well-formed diagram consisting of discrete and continuous blocks, if the expression function E of the continuous sub-diagram (consisting of the continuous blocks) satisfies the global Lipschitz condition, then the HUTP semantics of the entire diagram is determined and can be represented by a Simulink process. Proof. By Property 3 and Theorems 11 and 14, the HUTP semantics is a Simulink process. To show that the HUTP semantics of the combination of discrete and continuous sub-diagrams is determined, we perform an induction on multiples of the sample time st of the discrete sub-diagram (as defined in Lemma 17). At each step k, the computation of the discrete diagram provides the initial conditions at time k•st for evolution of the continuous diagram, and the continuous evolution provides the initial value for the discrete diagram at time (k + 1) • st. Hence determinacy follows from Lemma 17 and Lemma 18. Example 20. The connection of B 1 , B 2 (Example 12) and B 3 (Example 16) forms a closed Simulink diagram with the causality graph G = {(x, y), (y, z)} acyclic, hence the diagram is well-formed. Then, the HUTP semantics of this diagram is B 1 HUTP ∧ B 2 HUTP ∧ B 3 HUTP , expanding as follows:

Fig. 2 :

 2 Fig. 2: A well-formed Simulink diagram composed of two subsystems. The left is the original hierarchical diagram and the right is the flattened form.

  Fig. 5: A sketch of an enabled subsystem

Diagram

  HCSP = ConSubDiag DisSubDiag ConSubDiag = y := 0; a := 0; ȧ = y, ẏ = b&true ch a !a → skip ch b ?b → skip * DisSubDiag = t := 0;   t%2 == 0 → (ch a ?a; x := a + 1); t%3 == 0 → (b := x + 1; ch b !b); wait(1)   * where we now use to denote the parallel operator in HCSP (and use SIM to denote parallel operator on Simulink processes). As shown in Fig. 2 (right), the diagram consisting of two subsystems is flattened and then divided into two sub-diagrams: (1) the continuous sub-diagram ConSubDiag consisting of continuous blocks Int0 and Int1; (2) the discrete sub-diagram DisSubDiag consisting of discrete blocks Bias0 and Bias1. The parallel composition of ConSubDiag and DisSubDiag is by communication: ConSubDiag evolves along the ODEs ȧ = y, ẏ = b and then gets interrupted by the communication along ch a or ch b . It sends the value of a to DisSubDiag via channel ch a and receives the value of b from DisSubDiag via channel ch b . Notice that shared variables are not allowed in the context of HCSP. In the latest version of our tool chain MARS 1 , we implemented a new translation algorithm from Simulink to HCSP, avoiding the use of communication. Hence the Simulink diagram is translated to one sequential HCSP process. For the diagram in Fig. 2 (right), it is translated to the following process: Diagram HCSP = tt := 0; a := 0; y := 0; (10)   tt%2 == 0 → x := a + 1; tt%3 == 0 → b := x + 1; ȧ = y, ẏ = b, ṫt = 1&true 1 skip   +

,

  Diagram HCSP HUTP ≡ Diagram HUTP in two aspects: (1) there are more variables involved in Diagram HCSP HUTP , such as tt; (2) the duration of Diagram HCSP HUTP is always a positive integer (ti -ti = n ∈ N + ) but the one of Diagram HUTP can be any positive real number. Therefore, we formulate a notion of equivalence under which Diagram HCSP HUTP and Diagram HUTP can be considered to be equivalent. Definition 26 (Equivalence). Let Diagram be a Simulink diagram, S be the set of variables occurring in Diagram, and N be a positive integer. Then Diagram and its translation to HCSP, i.e., Diagram HCSP , are equivalent with respect to S until time N , if Diagram HCSP HUTP is equivalent to Diagram HUTP on the variables in S under the constraint ti -ti = N , denoted Diagram HCSP HUTP ≡ N,S Diagram HUTP If ∀N ∈ N + • Diagram HCSP HUTP ≡ N,S Diagram HUTP , then Diagram HCSP HUTP ≡ S Diagram HUTP Intuitively, we compare two HUTP representations (with potentially different alphabets) by projecting them on their shared variables first, and then by checking whether the two resulting representations are equivalent within the same duration.Since we are only concerned with the variables relating to the lines in the Simulink diagram, we let S = { Then we expand (ti -ti = N ) ∧ Diagram HUTP . Before expanding, we reformulate (ti -ti = N ) ∧ Subsystem0 HUTP to observe the finer-grained behaviour of Subsystem0, i.e., we shorten the step size of Subsystem0 from 2 to 1. Therefore,

∼

  y, ti , ti ) Therefore, we can get(ti -ti = N ) ∧ Diagram HUTP = (ti -ti = N )∧ Subsystem0 HUTP ∧ Subsystem1 HUTP which can expand to ti -ti = N ∧

  , ti ) and it can be proved that Diagram HCSP HUTP ≡ N,S Diagram HUTP for any N ∈ N + , i.e., Diagram HCSP HUTP ≡ S Diagram HUTP

  Thus, the hybrid process of the stateless discrete block is defined by

	DisBlock = (Comp Period) * Comp Tail
	where
	Tail =	∼ y = 0 ≤st
	means that the block can terminate at the times k • st or within the time
	intervals (k • st, (k + 1)st).
	For a stateful discrete block, its state variables s should be initialised,
	given by
	Init = [s = s 0 ]

  (2) if the function E satisfies the global Lipschitz condition, given any choice of input signals to the overall diagram, there are unique functions for all input, output, and state variables that satisfy the semantics.Proof.(1) Assume the diagram consists of m Integrator blocks and n computation blocks. Label the Integrator blocks by B i for 1 ≤ i ≤ m, and the computation blocks by B j for m + 1 ≤ j ≤ m + n. Let a i , s i and y i be the input, state and output variables of an Integrator block B i , respectively, and b j and c j be the input and output variables of a computation block B j , respectively. According to the semantics of these continuous blocks (see Section 4.2) and Property 15, the semantics of the diagram can be defined by

	Init ∧ Evolve	(6)
		5)
	where s 0 are the initial states of s,

∼ P is a relation only relating ∼ v, and E is a (vector) function in terms of variables in ∼ x ∼ s;

https://gitee.com/bhzhan/mars.git

Acknowledgement

This research is partly supported by NSFC under grant No. 62192732, 62192730, 62032024, and 61972385, and is also partly funded by Inria's joint research project CONVEX. The authors would like to thank the editors and anonymous reviewers, whose criticisms and suggestions did improve the presentation of our work very much.