SKLCS Xiong Xu

Shuling Wang
email: wangsl@ios.ac.cn

Bohua Zhan
email: bzhan@ios.ac.cn

Naijun Zhan

Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP

Keywords: CCS Concepts:, Theory of computation → Timed and hybrid models; Denotational semantics UTP, CPS, model-based design, semantic model

Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction however poses significant challenges. To address these issues, Hoare and He's Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design. Higher-Order UTP (HUTP) is a conservative extension to Hoare and He's theory which supports the specification of discrete, real-time and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of normal hybrid designs to model, analyse, compose, refine and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for HCSP (Hybrid Communicating Sequential Processes) and Simulink using HUTP.

INTRODUCTION

Hybrid systems, also known under the more architecture-centered denomination of cyber-physical systems (CPSs), exploit networked computing units to monitor and control physical processes via wired and/or radio communications. CPSs are omnipresent, from high-speed train control systems, power grids, automated factories, to ground, sea, air and space transportations. CPSs can be complex, networked, systems of systems, and are often entrusted with mission-and safety-critical tasks. variables in the paradigm. Higher-order quantifications over functions and predicates are also addressed in related works, such as [START_REF] Zeyda | A Modular Theory of Object Orientation in Higher-Order UTP[END_REF]. However, it is still unclear whether the classical UTP can be extended to hybrid systems like the extension to higher-order programs.

Our work starts from [START_REF] Chen | A Two-Way Path between Formal and Informal Design of Embedded Systems[END_REF], which extends UTP by allowing differential relations and higherorder quantification, establishing a theory of higher-order UTP (HUTP). Additionally, [START_REF] Chen | A Two-Way Path between Formal and Informal Design of Embedded Systems[END_REF] defines HUTP syntactically, which still leaves the question open of equipping it with an adequate algebraic structure (e.g., complete lattices) to serve as a semantics foundation for CPS design.

During the same period of [START_REF] Chen | A Two-Way Path between Formal and Informal Design of Embedded Systems[END_REF], to address the context of CPS design with UTP, Woodcock et al. introduce time-dependent trajectory variables into the alphabet and define hybrid relations [START_REF] Foster | Towards a UTP Semantics for Modelica[END_REF], based on which the semantics of Modelica [START_REF]Modelica ® -A Unified Object-Oriented Language for Systems Modeling (Language Specification)[END_REF] with a mixture of differential algebraic equations and event preemption is given. To unify discrete and hybrid theories, they introduce continuous-time traces to the trace model and define a generalised theory of reactive processes [START_REF] Foster | Unifying Theories of Time with Generalised Reactive Processes[END_REF] in terms of trace algebra. Subsequently in [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF], they define reactive design contracts that provide the basis for modelling and verification of reactive systems in the presence of parallelism and communication, yet limited to discrete controllers. Based on the theory of reactive processes, [START_REF] Foster | Hybrid Relations in Isabelle/UTP[END_REF] provides an alternative definition of hybrid relations to define a denotational semantics of hybrid programs [START_REF] Platzer | Logical Analysis of Hybrid Systems[END_REF]. However, the above bulk of works does not address some important features, including

• Super-dense computation. As argued in [START_REF] Maler | From Timed to Hybrid Systems[END_REF], super-dense computation provides a very appropriate abstract computation model for embedded systems, as computer is much faster than other physical devices and computation time of a computer is therefore negligible, although the temporal order of computations is still there. As [START_REF] Foster | Towards a UTP Semantics for Modelica[END_REF] considers finite timed traces with right continuity, super-dense time computation violates right continuity at time points, where a sequence of discrete events happen, and therefore cannot be modelled, although [START_REF] Foster | Unifying Theories of Time with Generalised Reactive Processes[END_REF] argues that the theory of finite timed traces is extensible to deal with infinite ones. • Parallelism with communication-based synchronisation is not addressed yet, although widely used in CPS designs. • Declaration of local variables and channels. Variables and channels are interpreted as functions over time, therefore declaration of local variables and channels have to resort to higher-order quantification. [START_REF] Foster | Automated Algebraic Reasoning for Collections and Local Variables with Lenses[END_REF] uses symmetric lenses to deal with local variables, but only discrete variables are considered.

For the drawbacks of our previous work [START_REF] Chen | A Two-Way Path between Formal and Informal Design of Embedded Systems[END_REF], we propose a new theory of HUTP and investigate the suitable algebraic structure for HUTP by taking all important features of hybrid systems into consideration, to enable its use as a semantics foundation for CPS design. Inspired by the Duration Calculus [START_REF] Zhou | A Calculus of Durations[END_REF], we introduce real-time variables, denoted as functions over time. Derivatives of real variables are additionally allowed in predicates, to form differential relations. In order to model synchronous communication between processes, we introduce timed traces to record the communication history of processes. Noteworthy contributions of previous works [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Foster | Unifying Theories of Time with Generalised Reactive Processes[END_REF][START_REF] Hoare | Unifying Theories of Programming[END_REF] with related aim regarded traces as finite abstract sequences. By contrast, timed traces in this paper can be infinite. Therefore, non-terminating behaviours such as divergence and deadlock can be described explicitly. These definitions ground the elaboration of the concepts of hybrid processes and (normal) hybrid designs, based on which we define formal semantics for HCSP [START_REF] He | From CSP to Hybrid Systems[END_REF][START_REF] Zhou | A Formal Description of Hybrid Systems[END_REF] and Simulink [START_REF]Simulink ® User's Guide[END_REF] using HUTP, and justify the correctness of the translation from Simulink to HCSP in [START_REF] Zou | Verifying Simulink Diagrams Via A Hybrid Hoare Logic Prover[END_REF] as an application of HUTP. In addition, by abstracting hybrid processes and (normal) hybrid designs, we propose a skeleton of equipping HUTP with compositional assume-guarantee reasoning by means of contracts.

Our work is similar to [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF] in some aspects, as both are extensions of traditional UTP [START_REF] Hoare | Unifying Theories of Programming[END_REF]. However, they differ in essence, namely:

• Our HUTP theory separates the concerns of time, state and traces. Especially, we introduce continuous state variables and construct a trace model to address concurrency and communication for hybrid systems. In [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Foster | Unifying Theories of Time with Generalised Reactive Processes[END_REF], although continuous states are encapsulated into traces, parallelism based on traces is not made explicit. For example, the interleaving of traces carrying continuous states is confusing, as, in reality, physical evolution never interleaves with discrete models. • Our approach can deal with infinite behaviour very well, in which therefore deadlock and divergence can be modelled formally. For example, the Zeno's paradox (Example 3.5) can be modelled as a normal non-terminating (and not necessarily unpredictable) behaviour. In contrast, it is unclear how to model the Zeno's paradox and other infinite behaviours using [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF], as it seems that only finite traces are involved. • Since our HUTP theory supports infinite behaviours, auxiliary variables wait and wait ′ , denoting reactivity in discrete models [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Hoare | Unifying Theories of Programming[END_REF], are interpreted explicitly with our approach. In summary, our proposed HUTP is a conservative extension to the classical UTP of [START_REF] Hoare | Unifying Theories of Programming[END_REF] and contributes:

• the separation of concerns in hybrid system design into time, state and trace;

• a timed trace model recording execution history and captures communication behaviours;

• 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; • higher-order quantification for specifying locality; • a calculus of hybrid processes and (normal) hybrid designs to model and analyse hybrid systems with (potentially) infinite behaviours; and • the HUTP semantics of HCSP and Simulink. Paper Organisation. The rest of the paper is organised as follows. Section 2 retrospects some preliminary concepts of the Unifying Theories of Programming. Section 3 defines a timed trace model which will play an important role in the HUTP theory. Section 4 introduces hybrid processes which combine time, states and traces to provide a uniform semantics for hybrid systems. To elaborate a sound theory, we extend hybrid processes to (normal) hybrid designs in Section 5. In Section 6, the HUTP is applied to verify the translation from Simulink diagrams to HCSP as an application of HUTP. Section 7 addresses the related work and Section 8 concludes this paper and discusses future works.

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 𝛼 (𝑃), containing its variables 𝑥 and primes 𝑥 ′ , and a relational predicate 𝑃 referring to this vocabulary. The terms 𝑥 and 𝑥 ′ are called observable variables: 𝑥 is observable at the start of execution and 𝑥 ′ is observable at the end of execution. The behaviour of a program is encoded as a relation between the observable variables 𝑥 and 𝑥 ′ . 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 ′ \{𝑥 ′ }) denotes excluding 𝑥 (𝑥 ′ ) from x (x ′ ). To start with, the relation calculus comprises all operators of first-order logic.

𝑥 𝑒 = 𝑥 ′ = 𝑒 ∧ x ′ \{𝑥 ′ } = x\{𝑥 } 𝑃 𝑄 = ∃x * • 𝑃 [x * /x ′ ] ∧ 𝑄 [x * /x] 𝑃 ◁ 𝑏 ▷ 𝑄 = (𝑏 ∧ 𝑃) ∨ (¬𝑏 ∧ 𝑄) 𝑃 ⊓ 𝑄 = 𝑃 ∨ 𝑄 𝑃 ⊔ 𝑄 = 𝑃 ∧ 𝑄
Assignment 𝑥 𝑒 is defined by observing the update 𝑥 ′ of variable 𝑥 once its value 𝑒 is evaluated, leaving other variables in the alphabet x unchanged. Sequence 𝑃 𝑄 is modelled by locally binding, through x * , the final state x ′ of 𝑃 and the initial state x of 𝑄 both are instantiated to it. Note that requires that 𝛼 out (𝑃) = 𝛼 ′ in (𝑄), where 𝛼 out (𝑃) and 𝛼 in (𝑄) denote the sets of output and input variables in 𝛼 (𝑃) and 𝛼 (𝑄), respectively, and 𝛼 ′ in (𝑄) is the primed version by priming all the variables in 𝛼 in (𝑄). The conditional 𝑃 ◁ 𝑏 ▷ 𝑄 evaluates as 𝑃 if 𝑏 is true or as 𝑄 otherwise. 𝑃 ⊓ 𝑄 non-deterministically chooses 𝑃 or 𝑄, whereas 𝑃 ⊔ 𝑄 is a conjunction of 𝑃 and 𝑄.

Let 𝑃 and 𝑄 be two predicates with the same alphabet, say {x, x ′ }. Then, 𝑄 is a refinement of 𝑃, denoted 𝑃 ⊑ 𝑄, if ∀x, x ′ • 𝑄 ⇒ 𝑃. In addition, 𝑃 ⊑ 𝑄 iff 𝑃 ⊓ 𝑄 = 𝑃 iff 𝑃 ⊔ 𝑄 = 𝑄. With respect to the refinement order ⊑, the least (𝜇) and greatest (𝜈) fixed points of a program function 𝐹 can be defined as follows:

𝜇𝐹 = {𝑋 | 𝐹 (𝑋 ) ⊑ 𝑋 } 𝜈𝐹 = {𝑋 | 𝑋 ⊑ 𝐹 (𝑋 )}
Example 2.1. Given an alphabet {𝑥, 𝑦, 𝑥 ′ , 𝑦 ′ }, the semantics of the assignment 𝑥 1 is different from 𝑥 ′ = 1. The former is equivalent to 𝑥 ′ = 1 ∧ 𝑦 ′ = 𝑦, while the latter indicates that 𝑦 and 𝑦 ′ can be arbitrary, i.e., 𝑥 ′ = 1 ⊑ 𝑥 1. They are equivalent if the alphabet contains only 𝑥 and 𝑥 ′ .

A UTP theory is a well-defined subset of alphabetised relations that satisfies certain conditions, called healthiness conditions. If a predicate is a fixed point of the healthiness condition, 𝑃 = H(𝑃), then it is said to be H-healthy. In other words, a healthiness condition H defines an invariant predicate set {𝑋 | H(𝑋 ) = 𝑋 }, 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 with respect to the refinement order ⊑, 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 and, additionally, recursion can be well specified. Multiple healthiness conditions H 0 , H 1 , • • • , H 𝑛 can also be composed as

H = H 0 • H 1 • • • • • H 𝑛 ,
provided that H 𝑖 and H 𝑗 commute, for all 0 ≤ 𝑖, 𝑗 ≤ 𝑛. Healthiness conditions play an important role in UTP, and distinct healthiness conditions can be defined to specify properties of different programming paradigms. In Section 4, we use healthiness conditions to define the concept of hybrid processes.

Example 2.2. Given an alphabet {𝑥, 𝑥 ′ , term, term ′ }, where the Boolean variable term ′ denote whether the program has terminated. If the preceding program is non-terminated (¬term), the current program 𝑃 should do nothing but keep the values of all variables unchanged, expressed by the following healthiness condition:

H (𝑃) = 𝑃 ◁ term ▷ (𝑥 ′ = 𝑥 ∧ term ′ = term)
The statement 𝑥 1 is not H -healthy, but we can make it H -healthy by

H (𝑥 1) = (𝑥 1) ◁ term ▷ (𝑥 ′ = 𝑥 ∧ term ′ = term)
It is easy to check that the above program is indeed a fixed point of 𝑋 = H (𝑋 ). When term is true, i.e., the preceding program is terminated, the above program executes 𝑥 1. Note that this assignment is equivalent to

𝑥 ′ = 1 ∧ term ′ = term. If non-termination is expected, we can write H (𝑥 ′ = 1 ∧ ¬term ′ ). It is a left-zero of sequential composition, i.e.,

H (𝑥

′ = 1 ∧ ¬term ′ ) 𝑃 = H (𝑥 ′ = 1 ∧ ¬term ′ )
provided that 𝑃 is any H -healthy predicate whose alphabet is {𝑥, 𝑥 ′ , term, term ′ }.

Following the convention of UTP, in this paper, we will define a set of healthiness conditions to identify the features of hybrid systems. The operators for classical sequential programs based on first-order relational calculus, such as , ⊓ and ⊔, can be easily lifted to the theory for hybrid systems proposed in this paper based on higher-order differential relational calculus, and we will prove that they still hold the desired properties like in classical UTP.

TIMED TRACE MODEL

In this section, we construct a timed trace model to capture the communication behaviour of processes. Traces play an important role in our HUTP theory which separates the concerns of time, state and trace. For processes in parallel, we assume that no shared variable is allowed between them and exchange of data between processes is described solely by communications. The synchronous communication between concurrent processes is achieved using input and output data channels. The input action ch?𝑥 receives a value along channel ch and assigns it to the variable 𝑥, and the output action ch!e sends the value of the expression 𝑒 along channel ch. A synchronous communication takes place immediately when both the sending and the receiving actions are enabled. If one party is not ready, the other has to wait.

Trace Blocks

Each timed trace is a sequence of communication, wait and internal blocks defined below:

• A pair ⟨ch * , 𝑑⟩ is a communication block, where ch * , a channel operation, indicates input (ch?), output (ch!) or synchronised communication (ch), and 𝑑 is a value along channel ch.

It represents that a communication along ch * takes place instantly. For example, ⟨ch?, 𝑑⟩ describes the communication receiving the value 𝑑 along the channel ch at current time. • A pair ⟨𝛿, RS⟩ is a wait block, where 0 < 𝛿 ≤ +∞ is the time period and RS is a set of waiting channel operations, called ready set. It means the process evolves during the period with the channel operations in RS ready for communication. The dual of RS is defined by

RS = {ch * | ch * ∈ RS, * ∈ {?, !}}
where ? = ! and ! = ?, and we assume that RS ∩ RS = ∅. • The symbol 𝜏 is an internal block standing for an internal or invisible action such as a timeless discrete computation.

Example 3.1. For the communication of two HCSP processes: ch?𝑥 ∥ch!2, since ch?𝑥 and ch!2 are ready simultaneously at the beginning, the communication takes place instantly according to the semantics of HCSP [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF]. The timed traces of ch?𝑥 and ch!2 are ⟨ch?, 2⟩ and ⟨ch!, 2⟩, respectively. Example 3.2. Consider the delay communication ch?𝑥 ∥ (wait 1; ch!2). Since the right process waits for 1 time unit before ch!2 is ready, the left process has to wait for 1 time unit for synchronisation although it has been ready since the beginning. The communication takes place after 1 time unit. Therefore, the timed trace of the left is ⟨1, {ch?}⟩ ⌢ ⟨ch?, 2⟩ and the right is ⟨1, ∅⟩ ⌢ ⟨ch!, 2⟩. The assignment 𝑥 1 is a timeless discrete action denoting initialisation. The left HCSP process means the continuous evolution depicted by the ODE 𝑥 = 𝑥 is preempted as soon as the communication sensor!𝑥 takes place, followed by actuator?𝑥. The right process indicates that the ODE of the left process evolves for 2 time units before sensor!𝑥 takes place when the value of 𝑥 reaches exp [START_REF] Abrial | Formalizing Hybrid Systems with Event-B[END_REF]. Therefore, the timed trace of the left process is and the timed trace of the right process is ⟨2, ∅⟩ ⌢ ⟨sensor?, exp(2)⟩ ⌢ ⟨actuator!, exp(2) + 1⟩

𝜏 ⌢ ⟨2, {sensor!}⟩ ⌢ ⟨sensor!, exp(

Timed Traces

In the previous works such as [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Foster | Unifying Theories of Time with Generalised Reactive Processes[END_REF][START_REF] Hoare | Unifying Theories of Programming[END_REF], traces are finite sequences. In our work, we consider infinite timed traces. A timed trace is a finite or infinite sequence of communication, wait, and internal blocks which records the execution history of a process.

Let Σ be the set of all channels and Σ? and Σ! the respective sets of receiving and sending events along channels in Σ. The sets of communication and wait blocks are respectively

C = (Σ? ∪ Σ! ∪ Σ) × D W = {⟨𝛿, RS⟩ | 0 < 𝛿 ≤ +∞, RS ⊆ (Σ? ∪ Σ!), RS ∩ RS = ∅}
where D is some domain.

Definition 3.4 (Timed Trace Set). Let TT = (C ∪ W ∪ {𝜏 }) * ∪ (C ∪ W ∪ {𝜏 }) 𝜔
be the timed trace set, 𝜖 the empty trace and ⌢ the concatenation between trace blocks. Then, the algebra (TT, 𝜖, ⌢ ) satisfies the following axioms, where ⌢ takes precedence over =.

Associativity

∀tt 0 , tt 1 , tt 2 ∈ TT • (tt 0 ⌢ tt 1 ) ⌢ tt 2 = tt 0 ⌢ (tt 1 ⌢ tt 2 ) Unit ∀tt ∈ TT • 𝜖 ⌢ tt = tt ⌢ 𝜖 = tt Left Zero ∀tt ∈ TT • ⟨+∞, RS⟩ ⌢ tt = ⟨+∞, RS⟩ Additivity ⟨𝛿 0 , RS⟩ ⌢ ⟨𝛿 1 , RS⟩ = ⟨𝛿 0 + 𝛿 1 , RS⟩
The axiom Left Zero reflects a simplifying function lz : TT → TT that removes the redundant tail from each trace. For example, lz(⟨+∞, RS⟩ ⌢ ⟨2, RS⟩) = ⟨+∞, RS⟩. The axiom Additivity reflects a simplifying function add : TT → TT that merges all the consecutive wait blocks with the same ready set in each trace. For example, add (⟨1, RS⟩ ⌢ ⟨2, RS⟩) = ⟨3, RS⟩. Then, the composite function add • lz : TT → TT returns the simplest form of each trace. A trace tt is called canonical normal form if |tt| = |add • lz(tt)|, where | • | returns the length of traces. Thus, we say tt is canonical if it cannot be simplified. In what follows, all traces are referred to canonical normal form if not otherwise stated.

We say tt 0 is equivalent to tt 1 , denoted by tt 0 = tt 1 , if each finite prefix of tt 0 is also a prefix of tt 1 , and vice versa. We say tt 0 < tt 1 if tt 0 is finite and there exists a trace tt such that tt 0 ⌢ tt = tt 1 , and in addition we let tt 1tt 0 = tt. Therefore, tt 0 < tt 1 means tt 0 is a finite prefix of tt 1 , and tt 1tt 0 denotes the suffix after deleting tt 0 . Let lim(tt) be the sum of the time periods of all the wait blocks in tt. If no wait block appears in tt, then we let limit(tt) = 0. A trace tt is non-terminated if lim(tt) = +∞ ∨ |tt| = +∞ and divergent if lim(tt) < +∞∧ |tt| = +∞. Let tt(𝑛) be the 𝑛-th (start from 0) block of tt. If |tt| < +∞, for any 𝑛 ≥ |tt| we let tt(𝑛) = tt(|tt| -1), i.e., the last block of tt. We say tt is deadlocked if

lim(tt) = +∞ ∧ ∃𝑁 ∈ N • ∀𝑛 ≥ 𝑁 • tt(𝑛) = ⟨𝛿, RS⟩ ∧ RS ≠ ∅ ( 1
)
where N is the set of natural numbers. (1) means that, from a certain time point, the process will be waiting for communication forever. Clearly, a deadlock is non-terminated because lim(tt) = +∞. This non-termination occurs because some channel operations are never matched. From the view of failures-divergence model [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], the standard denotational semantics for CSP, a ready set is exactly the dual of a refusal set, which contains the events (channel operations) that are not refused. Thus, (1) means that, from a certain time point, the dual channel operations in tt's ready set are always refused by the environment, which leads to a deadlock. Especially, if lim(tt) = +∞ ∧ |tt| < +∞, the last block of tt must be a wait block ⟨+∞, RS⟩, in which case tt will be deadlocked if RS ≠ ∅.

Example 3.5 (Zeno's Paradox). Consider a ball falling from an initial height ℎ with initial velocity 0. The ball falls freely with its dynamics given by the ODE 𝑣 = -𝑔, where 𝑣 is the velocity and 𝑔 is the gravitational acceleration. After 2ℎ/𝑔 time units, it hits the ground (ℎ = 0) with 𝑣 = -2ℎ𝑔. Then, there is a discontinuous update in its velocity. This discrete change can be modelled as a mode switch with the update given by 𝑣 -𝑐 • 𝑣. This assumes that the collision is inelastic, and the velocity decreases by a factor 𝑐, for some appropriate constant 0 < 𝑐 < 1. Next, the ball bounces back with velocity 𝑐 2ℎ𝑔 and reaches the peak (𝑣 = 0) after 𝑐 2ℎ/𝑔 time units. The ball then falls again and this process repeats infinitely. In summary, the timed trace of the bouncing ball is

⟨ 2ℎ/𝑔, ∅⟩ ⌢ 𝜏 ⌢ ⟨2𝑐 2ℎ/𝑔, ∅⟩ ⌢ 𝜏 ⌢ • • • ⌢ ⟨2𝑐 𝑛+1 2ℎ/𝑔, ∅⟩ ⌢ 𝜏 ⌢ • • •
where the internal blocks (𝜏s) denote the mode switch of the velocity (𝑣 -𝑐 • 𝑣). The limit of this timed trace is 1+𝑐 1-𝑐 • 2ℎ/𝑔 but the length of it is infinite, i.e., a divergence.

Parallel Composition

For each pair of processes in parallel, we assume that they communicate over a set of channels 𝐼 . Concretely, they can only exchange messages or data synchronously via the channels in 𝐼 , and they communicate with the environment via channels outside 𝐼 . In [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], this parallel is called generalised or interface parallel, and in [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF], it is called alphabetised parallel and the channels in 𝐼 are called common channels. Therefore, in this paper, the set 𝐼 is called a common channel set between processes (traces). For simplicity, we also assume:

(1) Each input or output channel can only be owned by one sequential process, i.e., a channel operation like ch? cannot occur in two different sequential processes in parallel. (2) Any pair of symmetric input and output channels cannot be owned by one sequential process, i.e., channel operations like ch? and ch! cannot occur in one sequential process.

Such restrictions are not essential, as the general communication model can always be reduced to this simplified model, please refer to [START_REF] Hoare | Communicating Sequential Processes[END_REF] for the details. Let tt 0 ∥ 𝐼 tt 1 tt denote that the parallel composition of two timed traces tt 0 and tt 1 over a common channel set 𝐼 derives a new timed trace tt. Since infinite timed traces are included, we give the following coinductive rules to define the parallel composition of timed traces, where the binding priority among operators is that ⌢ prior to ∥ 𝐼 prior to , and ⊎ is a disjoint union.

𝜖 ∥ 𝐼 𝜖 𝜖 [Empty] ⟨𝛿, RS 0 ⟩ ⌢ tt 0 ∥ 𝐼 ⟨𝛿, RS 1 ⟩ ⌢ tt 1 ⟨𝛿, RS 0 ⊎ RS 1 ⟩ ⌢ tt RS 0 ∩ RS 1 = ∅ tt 0 ∥ 𝐼 tt 1 tt [SynWait] ⟨ch?, 𝑑⟩ ⌢ tt 0 ∥ 𝐼 ⟨ch!, 𝑑⟩ ⌢ tt 1 ⟨ch, 𝑑⟩ ⌢ tt ch ∈ 𝐼 tt 0 ∥ 𝐼 tt 1 tt [SynIO] ⟨ch * , 𝑑⟩ ⌢ tt 0 ∥ 𝐼 tt 1 ⟨ch * , 𝑑⟩ ⌢ tt ch ∉ 𝐼 tt 0 ∥ 𝐼 tt 1 tt [NoSynIO] 𝜏 ⌢ tt 0 ∥ 𝐼 tt 1 𝜏 ⌢ tt tt 0 ∥ 𝐼 tt 1 tt [𝜏-Act]
Rule [Empty] says that the parallel composition of two empty traces trivially reduces to an empty trace. Rule [SynWait] states that when both sides are waiting for a communication, they can be synchronised for the same length of period if their ready sets are unmatched, i.e., RS 0 ∩ RS 1 = ∅, because RS 0 ∩ RS 1 ≠ ∅ indicates that the two sides are waiting for a communication with some channel operations matched, that should be taken immediately, and no time synchronization is allowed. Rule [SynIO] synchronises the input and output communications along some channel ch ∈ 𝐼 . The synchronization will never be applied to channels outside 𝐼 or internal actions 𝜏 as stated by Rules [NoSynIO] and [𝜏-Act]. In addition, there are symmetric versions of these rules, which means that ∥ 𝐼 is commutative. Property 1 (Associativity). Let 𝐼 0 , 𝐼 1 and 𝐼 2 be the respective common channel sets between timed traces tt 0 and tt 1 , tt 1 and tt 2 , and tt 2 and tt 0 , then

(tt 0 ∥ 𝐼 0 tt 1 ) ∥ 𝐼 1 ⊎𝐼 2 tt 2 = tt 0 ∥ 𝐼 0 ⊎𝐼 2 (tt 1 ∥ 𝐼 1 tt 2 ).
Example 3.6. The timed trace tt 0 = ⟨2, {ch?}⟩ ⌢ ⟨ch?, 5⟩ indicates a delay for 2 time units, during which the channel operation ch? is waiting, followed by receiving the value 5 along channel ch. The trace tt 1 = ⟨2, ∅⟩ ⌢ ⟨ch!, 5⟩ indicates a delay for 2 time units, during which no channel operations are waiting, followed by sending the value 5 along channel ch. The parallel composition of tt 0 and tt 1 over the channel ch is

tt 0 ∥ {ch} tt 1 ⟨2, {ch?}⟩ ⌢ ⟨ch, 5⟩ by [SynWait],
[SynIO] and [Empty]. In fact, recording ch? in the ready set of the composed traces is not necessary, as ch is a channel that only connects tt 0 and tt 1 , making it impossible for the environment to synchronise with it via ch. However, on the other hand, recording ch? has no side effect, and just indicates that the process itself was waiting for the channel operation ch! during the period, no matter whether ch is a common channel between tt 0 and tt 1 or not. This notion is in accordance to the semantics of HCSP (please refer to [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF] for the details).

Example 3.7. The timed trace tt 0 = ⟨dh?, 3⟩ ⌢ ⟨2, ∅⟩ indicates receiving the value 3 along channel dh at the initial time, followed by a delay of 2 time units during which no channel operations are waiting. Let tt 1 = ⟨1, ∅⟩ ⌢ ⟨1, {ch?}⟩. Then, we have

tt 0 ∥ {ch} tt 1 ⟨dh?, 3⟩ ⌢ ⟨1, ∅⟩ ⌢ ⟨1, {ch?}⟩ by [NoSynIO], [SynWait],
[Empty] and Additivity of wait blocks (see Definition 3.4). Note that if tt 0 and tt 1 also communicate via dh, then no rules can be applied for tt 0 ∥ {ch,dh} tt 1 because dh? cannot be synchronised, i.e., they are uncomposable.

Example 3.8. Let tt 0 = ⟨ch?, 3⟩ ⌢ ⟨dh?, 4⟩ and tt 1 = ⟨ch!, 3⟩ ⌢ ⟨dh!, 5⟩, then no rules can be applied for tt 0 ∥ {ch,dh} tt 1 as the values along channel dh are different although the heads of tt 0 and tt 1 are matched by [SynIO], i.e., tt 0 and tt 1 are uncomposable. Example 3.9. Let tt 0 = ⟨1, {ch?}⟩ and tt 1 = ⟨1, {ch!}⟩, then no rules can be applied for tt 0 ∥ {ch} tt 1 , as it is impossible that the symmetric channel operations ch? and ch! are waiting simultaneously, indicating that tt 0 and tt 1 are uncomposable.

Example 3.10. Consider two infinite timed traces

tt 0 = ⟨ch?, 0⟩ ⌢ ⟨ch?, 1⟩ ⌢ • • • ⟨ch?, 𝑛⟩ ⌢ • • • tt 1 = 𝜏 ⌢ ⟨ch!, 0⟩ ⌢ 𝜏 ⌢ ⟨ch!, 1⟩ ⌢ • • • ⌢ 𝜏 ⌢ ⟨ch!, 𝑛⟩ ⌢ • • •
The timed trace tt 0 indicates that the process is receiving values along channel ch endlessly at current time. The timed trace tt 1 indicates the infinite sending events at current time and before each sending event there is an internal action. Their parallel composition over ch is also infinite:

tt 0 ∥ {ch} tt 1 𝜏 ⌢ ⟨ch, 0⟩ ⌢ 𝜏 ⌢ ⟨ch, 1⟩ ⌢ • • • ⌢ 𝜏 ⌢ ⟨ch, 𝑛⟩ ⌢ • • • by [𝜏-Act] and [SynIO]
. It is a divergence as the time never progresses.

Example 3.11. Let tt 0 = 𝜏 ⌢ ⟨1, {ch?}⟩ ⌢ ⟨2, ∅⟩ and tt 1 = ⟨2, ∅⟩ ⌢ 𝜏 ⌢ ⟨1, {ch!}⟩. Then, their parallel composition via channel ch is

tt 0 ∥ {ch} tt 1 𝜏 ⌢ ⟨1, {ch?}⟩ ⌢ ⟨1, ∅⟩ ⌢ 𝜏 ⌢ ⟨1, {ch!}⟩ by [𝜏-Act],
[SynWait] and Additivity of wait blocks (see Definition 3.4). Notice that in this example, the symmetric channel operations ch? and ch! appear in one timed trace. Similar to Example 3.6, ch is a common channel between tt 0 and tt 1 and therefore it does not connect to the environment. ch? and ch! appearing in one timed trace is the result from parallel composition, which indicates this trace denotes a parallel process, not a sequential one. Actually, we can construct the following parallel HCSP processes:

P = 𝑥 0; ⟨ 𝑥 = 1&𝑥 < 1⟩ ⊵ (ch?𝑥 → skip); wait(2) Q = wait(2); 𝑦 0; ⟨ 𝑦 = 1&𝑦 < 1⟩ ⊵ (ch!𝑦 → skip)
The timed trace of P∥Q is exactly 𝜏 ⌢ ⟨1, {ch?}⟩ ⌢ ⟨1, ∅⟩ ⌢ 𝜏 ⌢ ⟨1, {ch!}⟩ as shown above.

HYBRID PROCESSES

Following Hehner's philosophy "programs as predicates" [START_REF] Hehner | A Practical Theory of Programming[END_REF], the first-order relational calculus of UTP [START_REF] Hoare | Unifying Theories of Programming[END_REF] can be used to model programs specified with possibly different or heterogeneous programming styles. In this section, we introduce continuous dynamics into rational predicates to model hybrid systems, and use the term hybrid processes to denote such extended predicates. Hybrid processes serve as the basis of the HUTP theory in this paper.

To use UTP for modelling hybrid systems' behaviours, one first needs to extend it with an explicit notion of time. This can be done by introducing two observational variables ti, ti ′ : R ≥0 ∪ {+∞} to specify the start-and end-time of the observed behaviour. Let tr ∈ add • lz(TT), where add • lz(TT) denotes the set of canonical normal traces, represent the timed trace before the process is started and tr ′ ∈ add • lz(TT) stand for timed trace up to the moment of observation.

In a real-time setting, process state variables are interpreted as functions over time. To specify its real-time value, we use ∼ 𝑠 to represent it. In a word, we have three versions for each state variable 𝑠:

• the version 𝑠 ∈ D stands for its initial value in the domain D, i.e., the input state variable, where D could be a Banach space; • the primed version 𝑠 ′ ∈ D stands for the final value, i.e., the output state variable; and • the real time version We use the boldface symbols s, s ′ , ∼ s and ∼ s to denote respective vectors of input, output, real-time state variables and the derivatives. The alphabet that our theory depends on is {ti, ti ′ , tr, tr ′ , s, ∼ s, ∼ s, s ′ } by default. Therefore, first-order predicate 𝑃 (x, x ′ ) introduced in Section 2 can be extended to high-order differential relation ∼ 𝑃 (ti, ti ′ , tr, tr ′ , s, ∼ s, ∼ s, s ′ ). By introducing some healthiness conditions for high-order differential relations, we can then define hybrid processes.

Healthiness Conditions

As stated in Section 2, healthiness conditions play an important role in UTP. Therefore, we introduce the following healthiness conditions to identify the features of hybrid processes:

• Time must be irreversible, and trace should be monotonically increasing because processes are not permitted to undo past events, i.e.,

H 0 (𝑋 ) = 𝑋 ∧ ti ≤ ti ′ ∧ tr ≤ tr ′
This healthiness condition is a variant of R1 of reactive processes in [START_REF] Hoare | Unifying Theories of Programming[END_REF] and [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF]. Here, however, R1 does not deal with time. Similar variants include HC1 in [START_REF] He | Concurrency, Security, and Puzzles -Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday[END_REF] and HCT1 in [START_REF] Foster | Towards a UTP Semantics for Modelica[END_REF], but they do not involve the concept of traces. • Trace should keep consistent with time:

H 1 (𝑋 ) = 𝑋 ∧ ti = lim(tr) ∧ ti ′ =
(𝑋 ) = (ti = ti ′ ∧ tr = tr ′ ) ◁ (ti = +∞ ∨ |tr | = +∞) ▷ 𝑋
where 𝑃 ◁𝑏 ▷𝑄 = (𝑏 ∧𝑃) ∨ (¬𝑏 ∧𝑄). This healthiness condition is similar to R3 in [START_REF] Hoare | Unifying Theories of Programming[END_REF] and R3 ℎ in [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF], except that we specify the auxiliary variable wait explicitly as ti = +∞ ∨ |tr | = +∞. Hence, unlike in classical UTP, variables wait and wait ′ are not used in our HUTP.

(𝑋 ) = 𝑋 ∧ RC ∧ SD where RC = ∀𝑖 • ∀𝑡 ∈ [ti, ti ′ ) • ∼ s 𝑖 (𝑡) = ∼ s 𝑖 (𝑡 + ) SD = ∀𝑖 • ∀𝑡 ∈ (ti, ti ′ ) • ∃𝑑 0 , 𝑑 1 • ∼ s 𝑖 (𝑡 -) = 𝑑 0 ∧ ∼ s 𝑖 (𝑡 + )
= 𝑑 1 denote the right-continuity and semi-differentiability, respectively, and s 𝑖 ( ∼ s 𝑖 and s ′ 𝑖 ) is the 𝑖-th variable in s ( ∼ s and s ′ ). H 4 rules out some ill behaviours, such as the Dirichlet function (returning 1 if 𝑡 is a rational number and 0 otherwise) and the Weierstrass function (continuous everywhere but differentiable nowhere). Definition 4.1 (Hybrid Process). A hybrid process HP is a fixed point of 𝑋 = H HP (𝑋 ), where

H HP = H 0 • H 1 • H 2 • H 3 • H 4 and the alphabet of HP is 𝛼 (HP) = {ti, ti ′ , tr, tr ′ , s, ∼ s, ∼ s, s ′ }.
Since wait and wait ′ , used to denote reactivity in discrete models [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Hoare | Unifying Theories of Programming[END_REF], are interpreted respectively as ti = +∞ ∨ |tr | = +∞ and ti ′ = +∞ ∨ |tr ′ | = +∞ in H 2 and H 3 , the hybrid processes defined by Definition 4.1 are essentially reactive. Theorem 4.2 (Idempotence and Monotonicity). H HP is idempotent and monotonic.

Operations

Meet and Join.

Let HP 0 and HP 1 be two hybrid processes. Non-determinism is simply modelled by logical disjunction:

HP 0 ⊓ HP 1 = HP 0 ∨ HP 1
It stands for a process that internally chooses to execute either HP 0 or HP 1 , regardless of the environment. The dual of non-determinism choice is conjunction:

HP 0 ⊔ HP 1 = HP 0 ∧ HP 1
The alphabets are expanded by ⊓ and ⊔, i.e., 𝛼 (HP 0 ⊓ HP 1 ) = 𝛼 (HP 0 ⊔ HP 1 ) = 𝛼 (HP 0 ) ∪ 𝛼 (HP 1 ).

In the literature, ⊓ is also called demonic choice or meet, while ⊔ is called angelic choice or join.

Generally, ⊓ means ∧ and ⊔ means ∨, but in UTP [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Hoare | Unifying Theories of Programming[END_REF], they always denote ∨ and ∧, respectively. Thus, in this paper, we will follow this notational convention.

Property 2. If HP 0 and HP 1 are H HP -healthy, then so are HP 0 ⊓ HP 1 and HP 0 ⊔ HP 1 .

Sequential

Composition. The sequential composition in traditional UTP can be adapted to hybrid processes:

HP 0 HP 1 = ∃ti * , s * , tr * • HP 0 [ti * , s * , tr * /ti ′ , s ′ , tr ′ ] ∧ HP 1 [ti * , s * , tr * /ti, s, tr] provided that 𝛼 out (HP 0 ) = 𝛼 ′ in (HP 1 )
, where 𝛼 out (HP 0 ) and 𝛼 in (HP 1 ) denote the sets of output and input variables (containing time and trace variables) in 𝛼 (HP 0 ) and 𝛼 (HP 1 ), respectively, and 𝛼 ′ in (HP 1 ) is the primed version by priming all the variables in 𝛼 in (HP 1 ). If 𝛼 out (HP 0 ) ≠ 𝛼 ′ in (HP 1 ), then we can extend the alphabets by 𝛼 + out (HP

0 ) = 𝛼 + in ′ (HP 1 ) = 𝛼 out (HP 0 ) ∪ 𝛼 ′ in (HP 1 )
to ensure the well-definedness of sequential composition. Property 3. If HP 0 and HP 1 are H HP -healthy, then so is HP 0 HP 1 .

With the definition of sequential composition, we can prove the following property for the healthiness condition H 3 defined before. Property 4. The healthiness condition H 3 is equivalent to

𝑋 = 𝑋 skip where skip = H 2 (ti = ti ′ ∧ tr = tr ′ ∧ s = s ′ ).

Complement. The complement of a hybrid process HP is interpreted by

¬ ≀ HP = H HP (¬HP)
Note that ¬HP is not H HP -healthy, as it may violate constraints such as tr ≤ tr ′ . Therefore, we enforce healthiness by H HP , resulting in ¬ ≀ HP. Intuitively, ¬ ≀ HP can be seen as the complement of HP in the context of hybrid processes, i.e., we can prove that ¬ ≀ HP⊓HP = ⊥ HP and ¬ ≀ HP⊔HP = ⊤ HP . Then we define implication by

HP 0 ⇒ ≀ HP 1 = ¬ ≀ HP 0 ∨ HP 1
These logic operators are similar to ¬ 𝑟 and ⇒ 𝑟 , used in [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF].

Quantification.

To support declaration, abstraction and instantiation of variables, as in [START_REF] Hoare | Unifying Theories of Programming[END_REF], we introduce quantifications over three versions 𝑠, 𝑠 ′ and ∼ 𝑠 of observable state variable 𝑠 in a hybrid process HP. Existential quantifications of first-order variables 𝑠 and 𝑠 ′ are as usual:

∃𝑠 • HP = {HP[𝑑/𝑠] | 𝑑 ∈ D} ∃𝑠 ′ • HP = {HP[𝑑/𝑠 ′ ] | 𝑑 ∈ D}
The quantification of real-time variable ∼ 𝑠 is of higher-order and it will meanwhile quantifies the derivative of ∼ 𝑠, as follows:

∃ ∼ 𝑠 • HP = HP[𝑓 , 𝑔/ ∼ 𝑠, ∼ 𝑠] 𝑓 : [ti, ti ′ ) → D 𝑔 : (ti, ti ′ ) ⇀ D ∀𝑡 ∈ (ti, ti ′ ) • 𝑓 (𝑡 -) = 𝑔(𝑡 -) ∧ 𝑓 (𝑡 + ) = 𝑔(𝑡 + )
Existential quantification removes the quantified variables from the alphabet of a process, i. Since real-time variables are functions over time, such quantifications are of higher-order (functional). It can also be proven that quantifiers ∃ and ∀ are H HP -preserving. In addition, higher-order ∃ and ∀ enjoy the following properties:

Property 5 (Quantification). ∃ ∼ 𝑥 • (HP 0 HP 1 ) = (∃ ∼ 𝑥 • HP 0 ) (∃ ∼ 𝑥 • HP 1 ) ∀ ∼ 𝑥 • (HP 0 HP 1 ) ⊒ (∀ ∼ 𝑥 • HP 0 ) (∀ ∼ 𝑥 • HP 1 ) ∃ ∼ 𝑥 • (HP 0 ⊓ HP 1 ) = (∃ ∼ 𝑥 • HP 0 ) ⊓ (∃ ∼ 𝑥 • HP 1 ) ∀ ∼ 𝑥 • (HP 0 ⊓ HP 1 ) ⊒ (∀ ∼ 𝑥 • HP 0 ) ⊓ (∀ ∼ 𝑥 • HP 1 ) ∃ ∼ 𝑥 • (HP 0 ⊔ HP 1 ) ⊑ (∃ ∼ 𝑥 • HP 0 ) ⊔ (∃ ∼ 𝑥 • HP 1 ) ∀ ∼ 𝑥 • (HP 0 ⊔ HP 1 ) = (∀ ∼ 𝑥 • HP 0 ) ⊔ (∀ ∼ 𝑥 • HP 1 ) ¬ ≀ ∃ ∼ 𝑥 • HP = ∀ ∼ 𝑥 • ¬ ≀ HP ¬ ≀ ∀ ∼ 𝑥 • HP = ∃ ∼ 𝑥 • ¬ ≀ HP
Note that in the above the refinement order ⊑ for predicates introduced in Section 2 can be lifted to hybrid processes naturally. With the aid of higher-order quantifiers, the lexical locality of a variable 𝑠 in a hybrid process HP can be specified by

local 𝑠 • HP = ∃𝑠, ∼ 𝑠, 𝑠 ′ • HP Example 4.3.
Consider a hybrid process with independent state variables 𝑥 and 𝑦:

HP 0 = H HP ti < ti ′ ∧ tr ′ -tr = ⟨ti ′ -ti, ∅⟩∧ 𝑥 = ∼ 𝑥 (ti) ∧ 𝑥 ′ = ∼ 𝑥 (ti ′-) ∧ 𝑦 = ∼ 𝑦 (ti) ∧ 𝑦 ′ = ∼ 𝑦 (ti ′-) ∧∀𝑡 ∈ (ti, ti ′ ) • ∼ 𝑥 (𝑡) = 1 ∧ ∼ 𝑦 (𝑡) = 2 with 𝛼 (HP 0 ) = {ti, ti ′ , tr, tr ′ , 𝑥, ∼ 𝑥, ∼ 𝑥, 𝑥 ′ , 𝑦, ∼ 𝑦, ∼ 𝑦, 𝑦 ′ }. A literal abstraction of variable 𝑥 from HP 0 is local 𝑥 • HP 0 = H HP ti < ti ′ ∧ tr ′ -tr = ⟨ti ′ -ti, ∅⟩∧ 𝑦 = ∼ 𝑦 (ti) ∧ 𝑦 ′ = ∼ 𝑦 (ti ′-) ∧ ∀𝑡 ∈ (ti, ti ′ ) • ∼ 𝑦 (𝑡) = 2
with the alphabet {ti, ti ′ , tr, tr ′ , 𝑦,

∼ 𝑦, ∼ 𝑦, 𝑦 ′ }.
Example 4.4. Consider another interesting example, let

HP 1 = H HP ti < ti ′ ∧ tr ′ -tr = ⟨ti ′ -ti, ∅⟩∧ 𝑥 = ∼ 𝑥 (ti) ∧ 𝑥 ′ = ∼ 𝑥 (ti ′-) ∧ 𝑦 = ∼ 𝑦 (ti) ∧ 𝑦 ′ = ∼ 𝑦 (ti ′-) ∧∀𝑡 ∈ (ti, ti ′ ) • ∼ 𝑥 (𝑡) + ∼ 𝑦 (𝑡) = 0 The abstraction of 𝑥 from HP 1 is local 𝑥 • HP 1 = H HP ti < ti ′ ∧ 𝑦 = ∼ 𝑦 (ti) ∧ 𝑦 ′ = ∼ 𝑦 (ti ′-) ∧ tr ′ -tr = ⟨ti ′ -ti, ∅⟩ with the alphabet {ti, ti ′ , tr, tr ′ , 𝑦, ∼ 𝑦, ∼ 𝑦, 𝑦 ′ }. Note that when 𝑥 is localised, the ODE ∼ 𝑥 (𝑡) + ∼ 𝑦 (𝑡) = 0 is also abstracted away.

Parallel Composition. The parallel composition of two hybrid processes is written as

HP 0 ∥ 𝑀 HP 1
which uses the parallel-by-merge scheme developed in UTP [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF][START_REF] Hoare | Unifying Theories of Programming[END_REF]. We assume that the state variables of concurrent processes are disjoint, i.e., 𝛼 (HP 0 )∩𝛼 (HP 1 ) = {ti, ti ′ , tr, tr ′ }. Let the notation HP 𝑋 make an 𝑋 -version of HP by adding the shared outputted variables (ti ′ and tr ′ ) in HP with the 𝑋 -subscript, i.e.,

HP 𝑋 = HP (ti = ti ′ 𝑋 ∧ tr = tr ′ 𝑋 ∧ s = s ′ ) = HP[ti ′ 𝑋 , tr ′ 𝑋 /ti ′ , tr ′ ]
Let s 0 and s 1 be state variables (s 0 ∩ s 1 = ∅) owned by hybrid processes HP 0 and HP 1 , respectively. Let s = s 0 ⊎ s 1 . Then, the parallel composition of HP 0 and HP 1 can be defined as follows:

HP 0 ∥ 𝑀 HP 1 = H HP (HP 0,𝑋 ∧ HP 1,𝑌 ∧ tr = tr ′ ) 𝑀
where 𝑀 is a merge predicate with 𝛼 (𝑀) = {ti 𝑋 , ti 𝑌 , ti ′ , tr 𝑋 , tr 𝑌 , tr, tr ′ , s, ∼ s, ∼ s, s ′ }. Therefore, the alphabet of the parallel composition is 𝛼 (HP 0 ∥ 𝑀 HP 1 ) = {ti, ti ′ , tr, tr ′ , s, ∼ s, ∼ s, s ′ }. The parallel-bymerge scheme is illustrated pictorially in Fig. 1.

$$ Fig. 1. Parallel-by-merge scheme (s = s 0 ⊎ s 1 )
From the above figure, we can see that by renaming the common dashed variables, two processes HP 0,𝑋 and HP 1,𝑌 execute independently and their respective outputs, as well as their common input trace tr, are fed into the merge predicate 𝑀. Then, 𝑀 produces the merged result as the output of the parallel composition. Each merge predicate reflects a corresponding parallel scheme, i.e., the parallel composition is parametric over 𝑀. Fig. 1 in this paper looks like Fig. 1 which illustrates the parallel-by-merge dataflow in [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF], because both of them are derived from the parallel-by-merge of the classic UTP of [START_REF] Hoare | Unifying Theories of Programming[END_REF], but they differ in the following two aspects:

(1) Continuous state variables ∼ s 0 and ∼ s 1 are involved and state variables s 0 and s 1 are disjoint (no sharing state variables) in our setting;

(2) We only transfer the input trace tr to the merge predicate, as it would be necessary in parallel composition (see Definition 4.5 for an example).

A merge predicate 𝑀 is well-defined if it satisfies the following three properties:

(1) 𝑀 = 𝑀 [ti 𝑋 , tr 𝑋 , s 0 , ti 𝑌 , tr 𝑌 , s 1 /ti 𝑌 , tr 𝑌 , s 1 , ti 𝑋 , tr 𝑋 , s 0 ], indicating ∥ 𝑀 is commutative. (2)
The end time of the parallel composition is infinite iff the end time of one process is infinite:

𝑀 = 𝑀 ∧ (ti ′ = +∞ ◁ (ti 𝑋 = +∞ ∨ ti 𝑌 = +∞) ▷ ti ′ < +∞)
(3) Similarly, the timed trace of the parallel composition is infinite iff the timed trace of one process is infinite:

𝑀 = 𝑀 ∧ (|tr ′ | = +∞ ◁ (|tr 𝑋 | = +∞ ∨ |tr 𝑌 | = +∞) ▷ |tr ′ | < +∞)
The following defines a well-defined merge predicate 𝑀 𝐼 that specifies parallelism. where

syn = ti ′ 𝑋 = ti 𝑋 ∧ ti ′ 𝑌 = ti 𝑌 ∧ s ′ 0 = s 0 ∧ s ′ 1 = s 1 ∧ tr ′ = tr∧ ti 𝑋 < ti 𝑌 ⇒ ∀𝑡 ∈ [ti 𝑋 , ti 𝑌 ) • ∼ s 0 (𝑡) = s 0 ∧ tr ′ 𝑋 = tr 𝑋 ⌢ ⟨ti 𝑌 -ti 𝑋 , ∅⟩ ∧ tr ′ 𝑌 = tr 𝑌 ∧ ti 𝑋 > ti 𝑌 ⇒ ∀𝑡 ∈ [ti 𝑌 , ti 𝑋 ) • ∼ s 1 (𝑡) = s 1 ∧ tr ′ 𝑋 = tr 𝑋 ∧ tr ′ 𝑌 = tr 𝑌 ⌢ ⟨ti 𝑋 -ti 𝑌 , ∅⟩ ∧ ti 𝑋 = ti 𝑌 ⇒ tr ′ 𝑋 = tr 𝑋 ∧ tr ′ 𝑌 = tr 𝑌 mrg = ti ′ = max{ti 𝑋 , ti 𝑌 } ∧ s ′ 0 = s 0 ∧ s ′ 1 = s 1 ∧ (tr ′ 𝑋 -tr) ∥ 𝐼 (tr ′ 𝑌 -tr) (tr ′ -tr)
The predicate syn synchronises the termination time (+∞ if non-terminated) of two processes. If ti 𝑋 < ti 𝑌 , then it delays the termination of the process tagged by 𝑋 until it reaches 𝑡 𝑌 . During the period of delay, the values of the corresponding state variables keep unchanged, and meanwhile the wait block ⟨ti 𝑌 -ti 𝑋 , ∅⟩ should be added to the end of the trace tr 𝑋 . Following syn is mrg which merges times, states and traces, respectively. It uses the maximum time as the termination time (+∞ if non-terminated) of the parallel composition (ti ′ = max{ti 𝑋 , ti 𝑌 }).

Property 6 (Well-Definedness). 𝑀 𝐼 is well-defined.

Complete Lattice

Property 7 (Monotonicity). The operators , ⊔, ⊓, ◁▷, ∃ and ∥ 𝑀 are monotonic and ¬ ≀ is anti-monotone, with respect to the refinement order ⊑.

A (finite or infinite) set S of hybrid processes equipped with the refinement order ⊑ forms a partially ordered set, denoted by (S, ⊑). Let S the disjunction of all hybrid processes in S, denoting a system that behaves as any of hybrid processes in S. Obviously, HP ⊑ S iff ∀𝑋 ∈ S • HP ⊑ 𝑋 . Conversely, the conjunction of all hybrid processes in S is denoted by S, which denotes a system that only has the behaviour shared by all hybrid processes in S. In lattice theory, S and S are called the infimum and supremum of a set S, respectively. Theorem 4.6 (Complete Lattice). Let HP be the image of H HP , i.e., it is the set of all hybrid processes, then it forms a complete lattice with top and bottom:

⊤ HP = HP = H HP (false) ⊥ HP = HP = H HP (true)
Recursion can be specified once a complete lattice is formed. Theoretically speaking, recursion can be denoted by the fixed points of the equation 𝑋 = 𝐹 (𝑋 ), where 𝐹 constructs the body of the recursion. If 𝐹 (𝑋 ) is monotonic, the fixed points of 𝑋 = 𝐹 (𝑋 ) form a complete lattice according to Knaster-Tarski theorem [START_REF] Tarski | A Lattice-Theoretical Fixpoint Theorem and Its Applications[END_REF]. The least fixed point is denoted by 𝜇𝑋 • 𝐹 (𝑋 ) and the greatest fixed point by 𝜈𝑋 • 𝐹 (𝑋 ). The definitions of the least and greatest fixed points refer to Section 2. In particular, 𝜇𝑋 • 𝑋 = ⊥ HP and 𝜈𝑋 • 𝑋 = ⊤ HP .

Non-termination, Deadlock, Divergence and Miracle

Non-termination has a special property, i.e., being a left zero of sequential composition: Definition 4.7 (Non-termination). A hybrid process HP is non-terminated iff HP HP = HP for any hybrid process HP.

A hybrid process is divergent if its execution time is finite but its trace is infinite; and a deadlock if its execution time is infinite with some channel operations waiting forever, specified as follows. It can be demonstrated that both divergence and deadlock are non-terminated by Definition 4.7.

DL(𝑋 ) = 𝑋 ∧ ti ′ = +∞ ∧ ∃𝑁 ∈ N • ∀𝑛 ≥ 𝑁 • tr ′ (𝑛) = ⟨𝛿, RS⟩ ∧ RS ≠ ∅
A miracle is a miraculous process that only occurs after a non-terminating hybrid process, and thus it is impossible to implement a miracle in reality. Formally, In contrast to the miracle, ⊥ HP is the most unpredictable behaviour, because it allows nondeterministically choosing a behaviour among possibly infinitely many processes; in other words, chaos. Generally, chaos is expected to be non-terminated (left-zero of sequential composition) and the parallel composition of any process with chaos should result in chaos (zero of parallel composition). However, the chaos ⊥ HP does not enjoy such desired properties as the miracle ⊤ HP does. This problem will be solved in Section 5.

Abstract Hybrid Processes

A hybrid process models the state and trace of a system over time to accurately render its concrete behavior. For the purpose of verification, however, such a level of detail is certainly excessive, as instead modular abstraction may be desired. To address this issue, we propose the notion of abstract hybrid process, where traces are simply abstracted. Formally, Definition 4.12 (Abstract Hybrid Process). An abstract hybrid process is a fixed point of

𝑋 = H a 0 • H a 2 • H a 3 • H 4 (𝑋 ) where H a 0 (𝑋 ) = 𝑋 ∧ ti ≤ ti ′ H a 2 (𝑋 ) = (ti = ti ′ ) ◁ ti = +∞ ▷ 𝑋 H a 3 (𝑋 ) = (∃s ′ • 𝑋 ) ◁ ti ′ = +∞ ▷ 𝑋
⊤ AHP = H a HP (false) ≡ ti = ti ′ = +∞ ⊥ AHP = H a HP (true) ≡ (ti = ti ′ ) ◁ ti = +∞ ▷ (ti ≤ ti ′ ∧ RC ∧ SD)
Clearly, ⊤ AHP ⊑ ⊤ HP and ⊥ AHP ⊑ ⊥ HP if we ignore the alphabets as ⊤ AHP and ⊥ AHP do not contain tr or tr ′ . Abstract hybrid processes also form a Boolean algebra (AHP, ⊓, ⊔, ¬ a ≀ , ⊤ AHP , ⊥ AHP ), where AHP is the image of H a HP and the negation ¬ a ≀ can be defined by ¬ a ≀ 𝑋 = H a HP (¬𝑋 ). Furthermore, an abstract hybrid condition is a fixed point of ¬ a ≀ 𝑋 = ¬ a ≀ 𝑋 ⊥ AHP . The equation can be denoted by a healthiness condition H a HC , i.e., a predicate is an abstract hybrid condition iff it is H a HC -healthy. Abstract hybrid conditions are a subset of abstract hybrid processes.

Additionally, by definition of the refinement relation, for a hybrid process HP with explicit timed traces, if 𝑃 ⊑ HP (ignoring the alphabets) then HP does satisfy the property 𝑃, which is represented by an abstract hybrid process. Hence, thanks to the lattice structure induced by ⊑, we can define an (𝛼, 𝛾) Galois-connection stipulating the concretisation of a property 𝑃 to be the meet of all hybrid processes that satisfy it, i.e., 𝛾 (𝑃) = {HP | 𝑃 ⊑ HP} and, dually, the abstraction of a hybrid process HP to be the join of all properties satisfied by it, i.e., 𝛼 (HP) = {𝑃 | 𝑃 ⊑ HP}. In particular, 𝛾 (⊥ AHP ) = ⊥ HP and 𝛼 (⊤ HP ) = ⊤ AHP .

HYBRID DESIGNS

In this section, we propose the concept of hybrid design. Hybrid designs are a subset of hybrid processes but enjoy some desired algebraic properties which are not featured by hybrid processes. Based on hybrid designs, we will then propose normal hybrid designs, which are the first-class notions in the HUTP theory.

The notion of design in UTP was first introduced by Hoare and He in [START_REF] Hoare | Unifying Theories of Programming[END_REF]. A design consists of a pair of predicates (Pre, Post) standing for the pre-and post-condition of a program, augmented with the Boolean variables ok and ok ′ to express whether the program has started and terminated:

Pre ⊢ Post = (ok ∧ Pre) ⇒ (ok ′ ∧ Post) ≡ ¬ok ∨ ¬Pre ∨ (ok ′ ∧ Post)
which states that if the program starts in a state satisfying the pre-condition Pre, it will terminate, and on termination the post-condition Post will be true. The pair (Pre, Post) describes a contract between the component and its environment, and therefore supports the decomposition of engineering tasks to resolve system design complexity.

In related works, the meanings of ok and ok ′ are slightly different. For example, in [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF], ok and ok ′ are used to indicate divergence. Here, however, since divergence can be observed from time and trace (ti ′ < +∞ ∧ |tr ′ | = +∞), ok and ok ′ have different meanings. We extend the notion of design to hybrid systems by interpreting ok and ok ′ to denote a process's status: ok ′ = true indicates that the process executes normally (not necessarily terminating), and hence ok = false means that the preceding process executed abnormally, causing the behaviour of the current process to be unpredictable. Thus, it is necessary to distinguish normal and abnormal non-termination. Specifically, ¬ok ′ indicates the abnormal behaviour, which should be abnormal non-termination;

ok ′ ∧ (ti ′ = +∞ ∨ |tr ′ | = +∞) indicates normal non-termination; and ok ′ ∧ ti ′ < +∞ ∧ |tr ′ | < +∞ indicates (normal) termination.
Definition 5.1 (Hybrid Designs). Let HP 𝐴 and HP 𝐶 be hybrid processes. Then,

HP 𝐴 ⊢ HP 𝐶 = (ok ∧ HP 𝐴 ) ⇒ ≀ (ok ′ ∧ HP 𝐶 )
is a hybrid design with the alphabet 𝛼 (HP 𝐴 ) ∪ 𝛼 (HP 𝐶 ) ∪ {ok, ok ′ }, where HP 𝐴 and HP 𝐶 are called assumption and commitment, respectively.

Hybrid designs are a subset of hybrid processes, as ok ∧ HP 𝐴 and ok ′ ∧ HP 𝐶 are H HP -healthy and ⇒ ≀ is H HP -preserving, which means HP 𝐴 ⊢ HP 𝐶 is also H HP -healthy. Intuitively, when a hybrid design starts normally (ok = true) and its assumption HP 𝐴 holds, then it executes normally and the commitment HP 𝐶 holds. The hybrid design ⊥ HP ⊢ HP 𝐶 , where ⊥ HP is a variant of true (which is a convention in UTP), is abbreviated as ⊢ HP 𝐶 meaning not making any assumptions.

Matrix Representation

Given a hybrid design HP 𝐴 ⊢ HP 𝐶 , if ok is false, i.e., its predecessor is abnormal, then it will behave unpredictably, i.e., chaos ⊥ HP ; if ok is true but ok ′ is false, it indicates that the assumption HP 𝐴 must be violated, i.e., ¬ ≀ HP 𝐴 ; if both ok and ok ′ are true, the commitment HP 𝐶 can be guaranteed as soon as the assumption HP 𝐴 holds, i.e., HP 𝐴 ⇒ ≀ HP 𝐶 . In order to make this semantics of hybrid designs clearer, we use the matrix encoding proposed in [START_REF] Möller | The Linear Algebra of UTP[END_REF] to define hybrid designs as 2 × 2 matrices by instantiating ok and ok ′ with all four possible combinations:

HP 𝐴 ⊢ HP 𝐶 = ¬ok ′ ok ′ ⊥ HP ⊥ HP ¬ok ¬ ≀ HP 𝐴 HP 𝐴 ⇒ ≀ HP 𝐶 ok (2)
With the aid of the matrix representation, the proofs of the theorems and properties on hybrid designs become more concise and intuitive. The proofs of this section are largely based on this matrix representation and the calculus on it (see the appendix for the details).

Normal Hybrid Designs

In general, UTP allows the assumption to refer to both primed and unprimed versions of variables. However, as explained in [START_REF] Guttmann | Normal Design Algebra[END_REF], only normal designs, whose assumptions are conditions and do not refer to primed (state) variables, are significant. Similarly, only normal hybrid designs, whose assumptions are fixed points of the equation below, make sense in hybrid system design.

¬ ≀ 𝑋 = ¬ ≀ 𝑋 ⊥ HP
Intuitively, the above equation indicates that if an execution violates an assumption, then we expect that any extension of the execution will also violate the assumption. For example, let HP be a hybrid process specifying the expected behaviour, then ¬ ≀ HP represents the unexpected behaviour. It is desirable that all the extensions of ¬ ≀ HP should also be unexpected, i.e., ¬ ≀ HP ⊑ ¬ ≀ HP ⊥ HP . Meanwhile, we have ¬ ≀ HP ⊥ HP ⊑ ¬ ≀ HP according to the monotonicity of (Property 7). In a word, we expect the property ¬ ≀ HP = ¬ ≀ HP ⊥ HP .

The above equation can be denoted by a healthiness condition

H HC (𝑋 ) = ¬ ≀ (¬ ≀ 𝑋 ⊥ HP )
A predicate is called a hybrid condition if it is H HC -healthy in a similar manner as reactive conditions in [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF]. Hybrid conditions are a subset of hybrid processes. For example, H HP (𝑠 > 0) is a hybrid condition while H HP (𝑠 ′ > 0) is not. Especially, ⊥ HP and ⊤ HP are hybrid conditions because it is easy to check that ⊥ HP = ¬ ≀ (¬ ≀ ⊥ HP ⊥ HP ) and ⊤ HP = ¬ ≀ (¬ ≀ ⊤ HP ⊥ HP ).

A hybrid design, say HC ⊢ HP, is called normal hybrid design, if HC is a hybrid condition (H HC -healthy). In what follows, we only consider normal hybrid designs. Operations on normal hybrid designs can be thus reduced to standard matrix operations. In particular, non-deterministic choice (meet) ⊓ and sequential composition correspond to matrix addition and multiplication, respectively. Moreover, reasoning is completely component-free (with no mention to ok and ok ′ or variable substitutions), i.e., compositional.

Theorem 5.2 (Operations).

(1) (HC 0 ⊢ HP 0 ) ⊓ (HC 1 ⊢ HP 1 ) = (HC 0 ∧ HC 1 ) ⊢ (HP 0 ∨ HP 1 ) (2) (HC 0 ⊢ HP 0 ) ⊔ (HC 1 ⊢ HP 1 ) = (HC 0 ∨ HC 1 ) ⊢ ((HC 0 ⇒ ≀ HP 0 ) ∧ (HC

1 ⇒ ≀ HP 1 )) (3) (HC 0 ⊢ HP 0 ) (HC 1 ⊢ HP 1 ) = (HC 0 ∧ ¬ ≀ (HP 0 ¬ ≀ HC 1 )) ⊢ (HP 0 HP 1 )
Parallel-by-merge, as defined for hybrid processes in Section 4.2.5, can naturally be extended to normal hybrid designs, except that the form of merge predicates should be adapted to deal with auxiliary variables ok and ok ′ . Concretely, the merge predicate for normal hybrid designs can be defined by:

NHD(𝑀) = (ok 𝑋 ∧ ok 𝑌 ) ⇒ ≀ (𝑀 ∧ ok ′ )
where 𝛼 (𝑀) ∩ {ok 𝑋 , ok 𝑌 , ok, ok ′ } = ∅. It states that only parallel designs execute normally (i.e. ok 𝑋 ∧ ok 𝑌 ) can they merge by 𝑀 as usual. Otherwise, merge becomes unpredictable.

(HC 0 ⊢ HP 0 ) ∥ NHD(𝑀) (HC 1 ⊢ HP 1 ) = ¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∧¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∧¬ ≀ (¬ ≀ HC 1 ∥ ⊥ HP HP 0 ) ⊢ HP 0 ∥ 𝑀 HP 1
Intuitively, the assumption of parallel composition, above, stipulates that unexpected interactions cannot happen. For example, ¬ ≀ HC 0 denotes the unexpected behaviour of HC 0 ⊢ HP 0 . Hence, its parallel composition with the behaviour of the other side, i.e., ¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 and ¬ ≀ HC 0 ∥ ⊥ HP HP 1 , should also be unexpected, as negated by the assumption, where the merge predicate ⊥ HP denotes the weakest parallelism, i.e., (P∥ ⊥ HP Q) ⊑ (P∥ 𝑀 Q) for any merge predicate 𝑀.

If state variables play the dominant role in the assumptions and traces are not the concern, such as H HP (𝑠 > 0), we can give an alternative definition to parallel composition as follows, which is simpler than ∥ NHD(𝑀) .

Definition 5.4 (Parallel Composition).

(HC 0 ⊢ HP 0 ) ∥ HP 𝑀 (HC 1 ⊢ HP 1 ) = (HC 0 ∧ HC 1 ) ⊢ (HP 0 ∥ 𝑀 HP 1 )

For normal hybrid designs, the assumption for non-chaos is made explicitly. Since parallel execution involves the evaluation of both processes, it is necessary to ensure that both their assumptions are valid to start with. Thus, the assumption for successful execution of the parallel composition is the conjunction of their separate assumptions rather than their disjunction. It states that the parallel composition HP 0 ∥ HP 𝑀 HP 1 can only be executed when both of the components successfully start with the assumptions HC 0 and HC 1 holding, otherwise, it is a chaos. Note that ∥ HP 𝑀 is different from ∥ NHD(𝑀) , the former composes assumptions and commitments separately while the latter treats hybrid designs as hybrid processes. This theorem indicates that the monotonic hybrid refinement relation can be lifted to a contravariant design refinement relation, and hence the monotonicity of modalities for normal hybrid designs can be proved, specified as the following two properties.

Property 10 (Contra-variance). If HC 0 ⊒ HC 1 and HP 0 ⊑ HP 1 then

(HC 0 ⊢ HP 0 ) ⊑ (HC 1 ⊢ HP 1 )
Property 11 (Monotonicity). Operators ⊔, ⊓, , ∥ NHD(𝑀) and ∥ HP 𝑀 for normal hybrid designs are monotonic with respect to ⊑.

Complete Lattice

The laws for ⊓ and ⊔ can be respectively generalised to and , which indicates that normal hybrid designs form a complete lattice, as stated by the following theorem. 2) its parallel composition with any normal hybrid design can result in itself (zero of parallel composition ∥ HP 𝑀 , see Property 15), which fixes the hole in the HUTP theory mentioned at the end of Section 4 (where the chaos ⊥ HP of hybrid processes does not enjoy such desired properties).

REFLECTION OF HCSP AND SIMULINK WITH HUTP

In this section, we give the HUTP semantics of HCSP [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF] and Simulink [START_REF]Simulink ® User's Guide[END_REF], representing two representative imperative and data-flow formalisms for hybrid system design in academia and industry, respectively. Furthermore, we prove the consistency between the operational semantics of HCSP and its HUTP semantics. We illustrate by an example the refinement relation between a Simulink diagram and the corresponding HCSP model within the HUTP framework, demonstrating the expressive capabilities of the UTP as a meta-theory for translation validation.

Syntactic Sugar

For brevity, we introduce the following syntax sugar for HUTP. We define the notations • and ⌈•⌋ which are similar to • and ⌈•⌉ of Duration Calculus [START_REF] Zhou | A Calculus of Durations[END_REF]. Let 𝑃 (

𝑃 (

∼ s, ∼ s), RS 𝜙 (ti,ti ′ ) = H HP ti < ti ′ < +∞ ∧ 𝜙 (ti, ti ′ ) ∧ s = ∼ s(ti) ∧ s ′ = ∼ s(ti ′-)∧ ∀𝑡 ∈ (ti, ti ′ ) • 𝑃 ( ∼ s(𝑡), ∼ s(𝑡)) ∧ tr ′ -tr = ⟨ti ′ -ti, RS⟩
is a finite continuous process over the time interval [ti, ti ′ ), and it says that ∼ s is differentiable with 𝑃 ( ∼ s, ∼ s) holding at every instant 𝑡 from ti to ti ′ . During the period, the channel operations in the ready set RS are waiting, recorded by the trace history tr ′ -tr. The predicate 𝜙 (ti, ti ′ ) characterises the relation of ti and ti ′ , such as ti ′ -ti = 2. We omit 𝜙 (ti, ti ′ ) if 𝜙 (ti, ti ′ ) = (ti < ti ′ ). For brevity,

𝑃 ( ∼ s, ∼ s), RS 𝑑 = 𝑃 ( ∼ s, ∼ s), RS ti ′ -ti=𝑑 𝑃 ( ∼ s, ∼ s), RS ∼𝑑 = 𝑃 ( ∼ s, ∼ s), RS (ti ′ -ti)∼𝑑
where 𝑑 > 0 and ∼ ∈ {<, ≤, ≠, >, ≥}. A sequence of operations which is assumed to take no time is called super-dense computation [START_REF] Maler | From Timed to Hybrid Systems[END_REF]. Under super-dense computation, the computer processing the sequence of the operations is much faster than the physical devices attached to it, rendering the time to compute the discrete operations negligible. However, the temporal order of computations is still present. Under the assumption of super-dense computation, a discrete process without communication is defined by

⌈𝑃 (s, s ′ )⌋ = H HP (ti = ti ′ < +∞ ∧ 𝑃 (s, s ′ ) ∧ tr ′ -tr = 𝜏)
It executes instantly at time ti = ti ′ < +∞, rather than continuously over a time interval. Especially,

⌈⌋ = H HP (ti = ti ′ < +∞ ∧ s = s ′ ∧ tr = tr ′ )
Note that ⌈⌋ ≠ ⌈s = s ′ ⌋ as their traces are different. We can prove the following property for ⌈⌋.

Property 16 (Unit). ⌈⌋ is a unit of hybrid processes w.r.t. .

Corollary 1 (Unit). ⊢ ⌈⌋ is a unit of normal hybrid designs w.r.t. . Instant communications can be defined by discrete processes with communication:

⌈ch?, s 𝑖 ⌋ = H HP (ti = ti ′ < +∞ ∧ ∃𝑑 • s 𝑖 𝑑 ∧ tr ′ -tr = ⟨ch?, 𝑑⟩) ⌈ch!, 𝑒 (s)⌋ = H HP (ti = ti ′ < +∞ ∧ s ′ = s ∧ tr ′ -tr = ⟨ch!, 𝑒 (s)⟩)
where s 𝑖 is the 𝑖-th variable in s and 𝑒 (s) is an expression containing s.

In addition, we also define infinite continuous processes:

𝑃 ( ∼ s, ∼ s), RS ∞ = H HP ti < ti ′ = +∞ ∧ s = ∼ s(ti)∧ ∀𝑡 ∈ (ti, +∞) • 𝑃 ( ∼ s(𝑡), ∼ s(𝑡)) ∧tr ′ -tr = ⟨+∞, RS⟩
Since we cannot observe the state variables of the point at infinity, the process will not output any values of state variables, i.e., the output state variables s ′ are hidden.

From HCSP to HUTP

HCSP is a formal language for describing hybrid systems. It extends Communicating Sequential Processes by introducing differential equations for modelling continuous evolutions and interrupts for modelling arbitrary interactions between continuous evolutions and discrete jumps. The syntax of HCSP is given as follows, adapted from [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF].

P skip | 𝑥 𝑒 | wait 𝑑 | ch?x | ch!e | 𝑋 | rec 𝑋 • P | P; P | P ⊓ P | 𝐵 → P | (3) ⟨𝐹 ( s, s) = 0&𝐵⟩ | ⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑑 P | ⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑖 ∈𝐼 (io i → P 𝑖 ) S P | S∥S
The HCSP constructs can be defined respectively by normal hybrid designs (Section 5.2) as follows:

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

skip HUTP = ⊢ ⌈⌋
It is a unit of normal hybrid designs w.r.t. by Corollary 1. • The assignment of the value 𝑒 to a variable 𝑥 is modelled as setting 𝑥 to 𝑒 and keeping all other variables constant if 𝑒 can be successfully evaluated [START_REF] Hoare | Unifying Theories of Programming[END_REF]. Therefore, the assignment can be interpreted as follows:

𝑥 𝑒 HUTP = E(𝑒) ⊢ ⌈𝑥 𝑒⌋
where E(𝑒) is H HC -healthy and specifies the condition by which 𝑒 can be evaluated. Note that 𝐸 is a function supplied for all expressions. For example, H HP (𝑠 ≠ 0) can be such a condition, where 𝑠 is a state variable in 𝑒.

• The wait statement will keep idle for 𝑑 time units keeping variables unchanged:

wait 𝑑 HUTP = ⊢ ∼ s = 0, ∅ 𝑑
• The sequential composition P 0 ; P 1 behaves as P 0 first, and if it terminates, as P 1 afterwards: P 0 ; P 1 HUTP = P 0 HUTP P 1 HUTP

• P 0 ⊓ P 1 denotes internal choice, which behaves as either P 0 or P 0 , and the choice is made by the process. It is interpreted as a demonic choice of two operands in a standard way: where N is the set of non-negative integers and P 0 = skip. • A continuous evolution statement ⟨𝐹 ( s, s) = 0&𝐵⟩ says that the process keeps waiting, and meanwhile keeps continuously evolving following the differential equations 𝐹 , until the domain constraint 𝐵 is violated:

P 0 ⊓ P 1 HUTP = P 0 HUTP ⊓ P 1 HUTP
⟨𝐹 ( s, s) = 0&𝐵⟩ HUTP = exit ⊓ (ode ∅ exit)
where

ode RS = ⊢ 𝐹 ( ∼ s, ∼ s) = 0 ∧ 𝐵 [ ∼ s/s], RS exit = ⊢ ⌈¬𝐵(s) ∧ s ′ = s⌋
Note that ode RS and exit take 𝐹 and 𝐵 as parameters. For brevity, the parameters are not shown in the following content. The above states that the process can either terminate at the beginning, i.e., exit, or evolve for a finite period before terminating without waiting communications, i.e., ode ∅ exit, depending on whether 𝐵 holds or not. • ⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑑 P behaves like ⟨𝐹 ( s, s) = 0&𝐵⟩, if the evolution terminates before 𝑑 time units. Otherwise, after 𝑑 time units of evolution according to 𝐹 , it moves on to execute P: It states that the process can either terminate or communicate at the beginning: exit ⊓ comm, evolve for a finite period before terminating or communicating: ode RS (exit ⊓ comm). • ch?x receives a value along channel RS and assigns it to 𝑥, and as the dual, ch!e sends the value of 𝑒 along channel RS: ch?x HUTP = ⟨ s = 0&true⟩ ⊵ (ch?x → skip) HUTP ch!e HUTP = ⟨ s = 0&true⟩ ⊵ (ch!e → skip) HUTP A communication takes place when both the sending and the receiving parties are ready, and may cause one side to wait if the other side is not ready. • P 0 ∥P 1 behaves as if sequential processes P 0 and P 1 run independently except that all communications along the common channels connecting P 0 and P 1 are to be synchronised. The processes P 0 and P 1 in parallel can neither share variables, nor input or output channels, i.e., a channel operation ch * appears in P 0 iff it does not appear in P 1 . The parallel composition of P 0 and P 1 can be translated as the parallel composition defined by Definition 5.4 with the merge predicate 𝑀 𝐼 defined by Definition 4.5: P 0 ∥P 1 HUTP = P 0 HUTP ∥ HP 𝑀 𝐼 P 1 HUTP [START_REF] Back | Refinement Calculus-A Systematic Introduction[END_REF] where 𝐼 is the set of common channels between P 0 and P 1 . In what follows we prove the consistency between the HUTP semantics and the structural operational semantics (SOS) of HCSP given in [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF]. The latter consists of a collection of transition rules of the following form 1 :

⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑑 P HUTP = exit ⊓ (ode ∅ <𝑑 exit) ⊓ (
Pre-condition

(P, (ti, s)) tb -→ (P ′ , (ti ′ , s ′ ), ∼ s)
where P and P ′ are HCSP processes, (ti, s) and (ti ′ , s ′ ) are process states, described by the state variables with timestamps, tb denote a trace block defined in Section 3, and ∼ s is a flow depicting the evolution from s to s ′ . Note that the flow ∼ s can be removed if the above transition describes a discrete action. For example, the SOS of an assignment is 𝑒 can be evaluated on s (𝑥 𝑒, (ti, s))

𝜏 -→ (𝜀, (ti, s[𝑥 ↦ → 𝑒 (s)])) 1 We here revise the operational semantics in [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF] where 𝜀 denotes termination. A more comprehensive understanding of the operational semantics can be found in [START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF]. We say the HUTP semantics and the SOS of an HCSP process are consistent iff they keep consistent on time, state and trace. Concretely, the changes of time and state and the generated trace of the SOS of an HCSP process should be reflected by its HUTP semantics, and vice versa. For example, the SOS for the ODE with communication interruption

ODE ⊵ = ⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑖 ∈𝐼 (ch 𝑖 * 𝑖 → P 𝑖 )
is described by the following rules:

¬𝐵(s) (ODE ⊵ , (ti, s)) 𝜏 - → (𝜀, (ti, s)) [Int0] ∼ s is a solution of 𝐹 ( s, s) = 0 ∼ s(ti) = s s ′ = ∼ s(ti ′-) ∀𝑡 ∈ [ti, ti ′ ) • 𝐵( ∼ s(𝑡)) (ODE ⊵ , (ti, s)) ⟨ti ′ -ti,{ch i ?,ch j ! |𝑖 ∈𝐼 ? ,𝑗 ∈𝐼 ! }⟩ --------------------→ (ODE ⊵ , (ti ′ , s ′ ), ∼ s) [Int1] 𝑖 ∈ 𝐼 ? ch 𝑖 * 𝑖 = ch 𝑖 ?𝑥 𝑖 (ODE ⊵ , (ti, s)) ⟨ch 𝑖 ?,𝑑 ⟩ ------→ (P 𝑖 , (ti, s[𝑥 𝑖 ↦ → 𝑑])) [Int2] 𝑗 ∈ 𝐼 ! ch 𝑗 * 𝑗 = ch 𝑗 !𝑒 𝑗 𝑒 𝑗 can be evaluated on s (ODE ⊵ , (ti, s)) ⟨ch 𝑗 !,𝑒 𝑗 (s) ⟩ ---------→ (P 𝑗 , (ti, s)) [Int3]
The rule [Int0] is reflected by exit and the rule [Int1] is reflected by ode RS ODE ⊵ HUTP , where RS = {ch i ?, ch j ! | 𝑖 ∈ 𝐼 ? , 𝑗 ∈ 𝐼 ! }. The rule [Int2], equivalent to ⊢ ⌈ch 𝑖 ?, 𝑥 𝑖 ⌋, depicts a receiving event that interrupts the ODE, followed by the process P 𝑖 . The HUTP semantics of P 𝑖 is denoted by P 𝑖 HUTP , and therefore, the HUTP semantics for the receiving event can be described by

⊢
ODE ⊵ = exit ⊓ comm ⊓ (ode RS ODE ⊵ )
In other words, the SOS of ODE ⊵ is equivalent to the equation 𝑋 = 𝐹 (𝑋 ), where

𝐹 (𝑋 ) = exit ⊓ comm ⊓ (ode RS 𝑋 )
Any solution of 𝑋 = 𝐹 (𝑋 ) can be treated as the HUTP semantics of ODE ⊵ . In this paper, we use the least fixed point:

𝜇𝑋 .𝐹 (𝑋 ) = exit ⊓ comm ⊓ ode RS (exit ⊓ comm)
as shown in (4). It can be checked that the SOS of ODE ⊵ , denoted by the above four transition rules, is reflected by (4), and vice versa.

Remark 1. Another solution of the equation

𝑋 = 𝐹 (𝑋 ) above is ode RS ∞ ⊓ exit ⊓ comm ⊓ (ode RS (exit ⊓ comm)) where ode RS ∞ = ⊢ 𝐹 ( ∼ s, ∼ s) = 0 ∧ 𝐵 [ ∼ s/s],
RS ∞ denotes ODE ⊵ will evolve forever, never terminate. This solution is reasonable, although it is neither the least nor the greatest fixed point. Theorem 6.1 (Semantic Consistency). The HUTP semantics of HCSP is consistent with the structural operational semantics of HCSP.

From Simulink to HUTP

Matlab/Simulink [START_REF]Simulink ® User's Guide[END_REF] is an industrial de-facto standard for modelling embedded systems. A Simulink diagram consists of a set of blocks. Each block has a set of input and output signals. A discrete block computes the output signal from the input signals periodically or aperiodically. A continuous block computes the output signal continuously by following a differential equation. Blocks can be organised into hierarchical subsystems, such as normal, triggered and enabled subsystems.

In this subsection, we introduce a formal semantics of Simulink by encoding it into HUTP. Overall, a Simulink diagram is split into discrete and continuous sub-diagrams which consist of discrete and continuous blocks, respectively. We define the respective semantics for the discrete and continuous sub-diagrams and then compose them together. The following Simulink diagrams serve as running examples. The left of Fig. 2 is the original diagram and the right is the diagram where the ports between some blocks are added.

Bias Gain Integrator0 Integrator1

Bias Gain Integrator0 Integrator1 port

Fig. 2. Examples of plant-control loop

Discrete Block. A discrete block is executed during a finite time interval. The left of Fig. 3 is the typical periodic discrete block of a math operation, such as Bias and Gain in Fig, 2. This kind of blocks are stateless. The block on the right is a periodic Unit Delay block, which is stateful.

Fig. 3. Discrete blocks

For each discrete block, we use ports to serve as channels for the input and output lines. For a periodic Math Operation block, periodically, one first gets data from the input ports (get), then performs a computation based on the inputs (comp), next puts the computed result to its output ports (put), and finally keeps silent for a period of time (period), as follows:

get = ⊢ ⌈in 0 ?, 𝑥⌋ ∧ G 0 (𝑥 ′ ) ⊢ ⌈in 1 ?, 𝑦⌋ ∧ G 1 (𝑦 ′ ) comp = A(𝑥, 𝑦) ⊢ ⌈𝑧 op(𝑥, 𝑦)⌋ put = ⊢ ⌈out 0 !, 𝑧⌋ ⊢ ⌈out 1 !, 𝑧⌋ period = ⊢ ∼ 𝑧 = 0, ∅ st
In the above, get acquires data 𝑥 and 𝑦 from channels (ports) in 0 and in 1 , respectively. Note that ⌈in 0 ?, 𝑥⌋ and ⌈in 1 ?, 𝑦⌋ are instant communications (i.e., fetch data whenever they require). The constraints G 0 (𝑥 ′ ) and G 1 (𝑦 ′ ) mean that only the desired data is received. Receiving does not consume time, so the order of channel operations in 0 ? and in 1 ? does not matter. comp denotes a computation, where A(𝑥, 𝑦) means that the operands 𝑥 and 𝑦, provided from get, must satisfy some assumption, such as 𝑦 ≠ 0. Therefore, the relation G 0 (𝑥) ∧ G 1 (𝑦) ⇒ A(𝑥, 𝑦) must hold. If A(𝑥, 𝑦) is satisfied, the computation ⌈𝑧 op(𝑥, 𝑦)⌋ executes. By contrast with get, put just puts the computed result to channels (ports) out 0 and out 1 . Note that get, comp and put do not consume ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022. time. Then, the process keeps quiescent for some period specified by the sample time st, denoted by period, where ∅ indicates the in 0 ?, in 1 ?, out 0 ! and out 1 ! are not ready to communicate with the context during the period. Finally, it can terminate at any time before the next period arrives (tail). In summary, a periodic Math Operation block can be translated as:

MOP = get comp put (period get comp put) * tail (6)
where

tail = ⊢ ∼ 𝑧 = 0, ∅ <st ⊓ ⊢ ⌈⌋
Unlike a Math Operation block, a Unit Delay block is stateful. The right of Fig. 3 is a typical periodic Unit Delay block. At the beginning, its state is initialised (init). Then, periodically, it puts the current state to the output channels (ports) out 0 and out 1 , then gets data from the input channel (port) in and updates the state (get), and finally holds the state for some period (period). In summary, a Unit Delay block can be translated as follows: For an Integrator block, the state is first initialised by an initial condition, as follows:

UnitDelay = init put get (period put get) * tail where init = ⊢ ⌈𝑦 init_y⌋ put = ⊢ ⌈out 0 !, 𝑦⌋ ⊢ ⌈out 1 !, 𝑦⌋ get = ⊢ ⌈in?, 𝑥⌋ ⊢ ⌈𝑦 𝑥⌋ period = ⊢ ∼ 𝑦 = 0, ∅ st tail = ⊢ ∼ 𝑦 = 0, ∅ <st ⊓ ⊢ ⌈⌋
init = ⊢ ⌈𝑦 init_y⌋
Then, its semantics depends on the context it interacts with:

• If the source block is continuous (such as Integrator0 in Fig. 2), then the block will evolve continuously following the ODE 𝑦 = 𝑥, instead of receiving 𝑥 periodically or aperiodically from the input port. Meanwhile, it will send the current value of 𝑦 to the output port out 1 whenever the non-continuous target block requires it (put). In that case, the corresponding HUTP semantics will be given as follows:

Integrator = init (put ⊓ ode 0 ) * (7)
where • On the other hand, if the source block is non-continuous (such as Integrator1 in Fig. 2), then, at each iteration, the block will either get data 𝑥 from the input channel (get), evolve according to the latest received data (ode 1 ), or put the current value of 𝑦 to the output channel (put), as follows:

put = ⊢ ⌈out 1 !, 𝑦⌋ ode 0 = ⊢ ∼ 𝑦 = ∼ 𝑥,
Integrator = init (get ⊓ put ⊓ ode 1 ) * (8)
where get = ⊢ ⌈in?, 𝑥⌋

ode 1 = ⊢ ∼ 𝑦 = ∼ 𝑥 ∧ ∼ 𝑥 = 0, {in?, out 1 !}
The semantics of a Math Operation block with sample time 0 in the right of Fig. 4 is a bit more complicated. It requires the conversions between discrete and continuous signals, as illustrated by Fig. 5. Concretely, the conversion of the discrete input signal 𝑦 0 to the continuous one (D/A converter) can be specified as follows:

converter0 = (⊢ ⌈in 1 ?, 𝑦 0 ⌋ ∧ G(𝑦 ′ 0 ) ⊢ ∼ 𝑦 0 = 0, {in 1 ?} ) *
At each iteration, converter0 gets the desired data (constrained by G(𝑦 ′ 0 )) from the input channel in 1 and then keeps the data unchanged for some period. Thus, the input 𝑦 0 can be treated as a continuous signal from the view of the continuous block.

On the other hand, the conversion of the continuous output signal 𝑧 1 to the discrete one (A/D converter) can be specified as follows:

converter1 = (⊢ ⌈out 1 !, 𝑧 1 ⌋ ⊢ ∃ ∼ 𝑑 • ∼ 𝑧 1 = ∼ 𝑑, {out 1 !} ) *
At each iteration, converter1 puts the current value of 𝑧 1 to the output channel out 1 and then 𝑧 1 continues evolving for some period. Thus, from the view of out 1 , the signal 𝑧 1 is discrete. Given that all the inputs and outputs are continuous, the computation of the continuous Math Operation block can be translated as follows: ⊢ ⌈⌋ denotes the case that simulation is not started (ti = ti ′ ). In summary, the semantics of the continuous Math Operation block of Fig. 5 can be described by the following parallel composition:

comp = A( ∼ 𝑥, ∼ 𝑦 1 ) ⊢ ∼ 𝑧 0 = op( ∼ 𝑥, ∼ 𝑦 1 ) ⊓ ⊢ ⌈⌋

It means that if the continuous inputs

CMOP = H share (converter0∥ ∅ comp∥ ∅ converter1)
where (1) ∥ ∅ denotes ∥ HP SYN ∅ with the merge predicate SYN ∅ = ti 𝑋 = ti 𝑌 ∧ 𝑀 ∅ . According to Definition 4.5, 𝑀 ∅ allows ti 𝑋 ≠ ti 𝑌 . However, blocks in Simulink are synchronous on time, i.e., ti 𝑋 = ti 𝑌 ;

(2) H share is the healthiness condition that enforces the consistency between ∼ 𝑦 0 and ∼ 𝑦 1 and between ∼ 𝑧 0 and ∼ 𝑧 1 when the diagram evolves, specified as follows:

H share (𝑃 ⊢ 𝑄) = 𝑃 ⊢ 𝑄 ∧ ∀𝑡 ∈ [ti, ti ′ ) • ∼ 𝑦 0 (𝑡) = ∼ 𝑦 1 (𝑡) ∧ ∼ 𝑧 0 (𝑡) = ∼ 𝑧 1 (𝑡)
As the parallel-by-merge in this paper (Section 4.2.5) does not support shared state variables, the healthiness condition above is used to enforce the parallel by shared state variables, i.e., it states that the evolutions of 𝑦 0 and 𝑧 0 should keep consistent with 𝑦 1 and 𝑧 1 , respectively, because 𝑦 1 and 𝑧 1 are respective aliases of 𝑦 0 and 𝑧 0 .

Lines between discrete Blocks.

In order to synchronise communications between discrete blocks, lines between blocks serve as buffers to receive data whenever source blocks provide and target blocks require, as illustrated by the buffer in Fig. 2. A typical buffer is shown below:

Discrete Discrete Discrete Fig. 6. A two-branch line between discrete blocks

Notice that the buffer must render the causality relation of ports (if the source block provides data and, meanwhile, a target block requires). It should guarantee that the target block can only get the latest data from the source block. In other words, if the channel operations out? and in 0 ! of the buffer occur simultaneously, out? should be earlier in 0 !. Therefore, buffer should be translated as follows: buffer = get (put 0 ⊓ put 1 ⊓ ready) * ready *

where get = ⊢ ⌈out?, 𝑥⌋ put 0 = ⊢ ⌈in 0 !, 𝑥⌋ put 1 = ⊢ ⌈in 1 !, 𝑥⌋ ready = ⊢ ∼ 𝑥 = 0, {out?, in 0 !, in 1 !} This means that, at each iteration, the buffer first gets data from the output port of the source block (get), then puts the received data to the input ports of the target blocks whenever they require it (put 0 and put 1 ), and finally waits for a period of time, during which channel operations out?, in 0 ! and in 1 ! are made ready for communication (ready).

Composition.

According to the above analysis, before translating the Simulink diagram on the left of Fig. 2, we need to add the necessary ports between some blocks, resulting in the diagram shown on the right of Fig. 2. Before execution, the system must be initialised by setting time to 0 and trace to 𝜖, as follows:

INIT = ⊢ H HP (ti ′ = 0 ∧ tr ′ = 𝜖)
Then, the composite system, the Diagram on the right of Fig. 2, can be defined in two parts. The Plant part consists of the continuous blocks Integrator0 and Integrator1. The Control part consists of the discrete blocks Bias and Gain, and a buffer between them. The Diagram can be modelled by the parallel composition of Plant and Control, as follows:

Plant = H share (Integrator0 ∥ ∅ Integrator1) (10) Control = Bias ∥ out 0 buffer ∥ in 1 Gain (11) Diagram HUTP = INIT (Plant ∥ {in 0 ,out 1 } Control) ( 12
)
where ∥ 𝐼 represents ∥ HP SYN 𝐼 with SYN 𝐼 = ti 𝑋 = ti 𝑌 ∧ 𝑀 𝐼 , for simplicity, and we use ∥ ch if 𝐼 = {ch}. It can be proved that SYN 𝐼 is well-defined from Property 6. In the above case,

H share (𝑃 ⊢ 𝑄) = 𝑃 ⊢ 𝑄 ∧ ∀𝑡 ∈ [ti, ti ′ ) • ∼ 𝑎 0 (𝑡) = ∼ 𝑎 1 (𝑡) = ∼ 𝑎(𝑡) (13)
because the continuous blocks Integrator0 and Integrator1 share 𝑎 which has two aliases 𝑎 0 and 𝑎 1 .

Example 6.2 (Algebraic Loop). Consider the loop of Bias and Gain in Fig. 7. It forms an algebraic loop. According to [START_REF] Benveniste | Contracts for System Design[END_REF], the respective prefixes of the communication traces of Bias and Gain are ⟨in 0 ?, 𝑑 0 ⟩ ⌢ 𝜏 ⌢ ⟨out 0 !, 𝑑 1 ⟩ and ⟨in 1 ?, 𝑑 2 ⟩ ⌢ 𝜏 ⌢ ⟨out 1 !, 𝑑 3 ⟩, where 𝜏 denotes timeless computations. According to [START_REF] Butterfield | State Visibility and Communication in Unifying Theories of Programming[END_REF], the prefixes of the communication traces of two buffers between Bias and Gain are ⟨out 0 ?, 𝑑 4 ⟩ ⌢ 𝜏 ⌢ ⟨in 1 !, 𝑑 5 ⟩ and ⟨out 1 ?, 𝑑 6 ⟩ ⌢ 𝜏 ⌢ ⟨in 0 !, 𝑑 7 ⟩. It can be verified that these four traces cannot be composed by ∥ 𝐼 , as defined in Section 3.3, which indicates that this unsound system will reduce to ⊤ HD , i.e., it can do nothing.

Bias

Fig. 7. A loop of discrete blocks

In addition to the above, the semantics of hierarchical diagrams, such as normal, triggered and enabled can also be defined using HUTP. Since describing their HUTP semantics clearly needs pages of space, they are not introduced in this paper. Note that compared with the HUTP semantics of Simulink given in [START_REF] Chen | A Two-Way Path between Formal and Informal Design of Embedded Systems[END_REF][START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF], the HUTP semantics defined above is much simpler with more solid foundations as HUTP theory is well developed in this paper.

Applying HUTP to Justify the Translation from Simulink to HCSP

In the work [START_REF] Zou | Verifying Simulink Diagrams Via A Hybrid Hoare Logic Prover[END_REF], we introduced how to translate Simulink (as well as Stateflow) diagrams to the corresponding HCSP models for the purpose of verifying them using a Hybrid Hoare Logic prover in Isabelle/HOL [START_REF] Zhao | Formal Verification of a Descent Guidance Control Program of a Lunar Lander[END_REF][START_REF] Zou | Formal Verification of Simulink/Stateflow Diagrams[END_REF]. The translation is automatic and is implemented as a module ss2hcsp in the tool chain MARS2 [START_REF] Bohua Zhan | Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander[END_REF][START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF] which implements the flow from modelling, simulation, verification to code generation for hybrid systems. In this subsection, we justify the correctness of the translation by ss2hcsp from the Simulink diagram of Fig. 2 to the corresponding HCSP model as an application of the HUTP proposed in this paper. Definition 6.3 (Conditional Equivalence). Let 𝑇 = {𝑡 𝑛 } ⊆ R ≥0 be a chain of increasing time points (𝑡 𝑛 < 𝑡 𝑛+1 ) with lim 𝑛→+∞ 𝑡 𝑛 = +∞ and 𝑆 the set of state variables. Let P and Q be differential relations. Then, we say P is equivalent to Q w.r.t. 𝑇 and 𝑆 iff P ∧ ti ′ ∈ 𝑇 is equivalent to Q ∧ ti ′ ∈ 𝑇 on the state variables in 𝑆, denoted by P ≡ 𝑇 ,𝑆 Q.

Intuitively, P ≡ 𝑇 ,𝑆 Q means that if P and Q terminate at time ti ′ ∈ 𝑇 , then their state variables in 𝑆 are consistent. In this subsection, we wish to justify Diagram HUTP ≡ 𝑇 ,𝑆 Diagram HCSP HUTP with some 𝑇 and 𝑆, where Diagram is the Simulink diagram of Fig. 2.

For the Simulink Diagram of Fig. 2, ss2hcsp generates the following HCSP process:

Diagram HCSP = Plant HCSP ∥Control HCSP
where

Plant HCSP = 𝑎 0; 𝑥 0 0; ⟨ 𝑥 0 = 𝑎, 𝑎 = 𝑧 1 , 𝑧 1 = 0&true⟩ ⊵ ch 𝑥 !𝑥 0 → skip, ch 𝑧 ?𝑧 1 → skip * Control HCSP = ti 0; ch 𝑥 ?𝑥 1 ; 𝑦 𝑥 1 + 1.5; 𝑧 0 𝑦 × 2.4; ch 𝑧 !𝑧 0 ; wait(1); ti%2 = 0 → (ch 𝑥 ?𝑥 1 ; 𝑦 𝑥 1 + 1.5); ti%3 = 0 → (𝑧 0 𝑦 × 2.4; ch 𝑧 !𝑧 0 ) *
The period of Control HCSP is the greatest common divisor (GCD) of periods of the blocks (Bias and Gain) it contains, i.e., GCD(2, 3) = 1, as denoted by wait(1). Since no shared variable is allowed between different HCSP processes in parallel, we let 𝑥 0 and 𝑥 1 be two aliases of 𝑥, and 𝑧 0 and 𝑧 1 the aliases of 𝑧, as shown by the right diagram in Fig. 2. We first study the conditions under which Plant HCSP is consistent with Plant of [START_REF] Chen | A Two-Way Path between Formal and Informal Design of Embedded Systems[END_REF]. According to (4), Plant HCSP can be translated as follows:

Plant HCSP HUTP = init 𝑎 init 𝑥 0 put 𝑥 ⊓ get 𝑧 ⊓ (ode (put 𝑥 ⊓ get 𝑧 )) * where init 𝑎 = ⊢ ⌈𝑎 0⌋, init 𝑥 0 = ⊢ ⌈𝑥 0 0⌋, put 𝑥 = ⊢ ⌈ch 𝑥 !, 𝑥 0 ⌋, get 𝑧 = ⊢ ⌈ch 𝑧 ?, 𝑧 1 ⌋ and ode = ⊢ ∼ 𝑥 0 = ∼ 𝑎 ∧ ∼ 𝑎 = ∼ 𝑧 1 ∧ ∼ 𝑧 1 = 0, {ch 𝑥 !, ch 𝑧 ?} (14)
According to ( 7) and ( 8), Plant of ( 10) can be unfolded as

Plant = H share (init 𝑥 0 (put 𝑥 ⊓ ode 0 ) * ) ∥ ∅ (init 𝑎 0 (get 𝑧 ⊓ ode 1 ) * ) (15)
where

init 𝑎 0 = ⊢ ⌈𝑎 0 0⌋, put 𝑥 = ⊢ ⌈in 0 !, 𝑥 0 ⌋, get 𝑧 = ⊢ ⌈out 1 ?, 𝑧 1 ⌋ and ode 0 = ⊢ ∼ 𝑥 0 = ∼ 𝑎 1 , {in 0 !} ode 1 = ⊢ ∼ 𝑎 0 = ∼ 𝑧 1 ∧ ∼ 𝑧
1 = 0, {out 1 ?} Note that in 0 and out 1 are the aliases of ch 𝑥 and ch 𝑧 , respectively, so we do not distinguish put 𝑥 and get 𝑧 in Plant HCSP HUTP and Plant. Now we demonstrate Plant of ( 15) is equivalent to

init 𝑎 init 𝑥 0 get 𝑧 ⊓ put 𝑥 ⊓ ode * (16)
if 𝜏s are removed from traces, where ode is defined in [START_REF] Foster | Automated Algebraic Reasoning for Collections and Local Variables with Lenses[END_REF]. The traces of init 𝑥 0 (put 𝑥 ⊓ ode 0 ) * and init 𝑎 0 (get 𝑧 ⊓ ode 1 ) * can be modelled by the finite state machines (FSMs) in Fig. 8, where 𝜏 𝑥 and 𝜏 𝑎 denote the actions of init 𝑥 0 and init 𝑎 0 , respectively. According to the definition of ∥ ∅ , the two FSMs in Fig. 8 only synchronise on wait blocks ⟨𝛿 𝑥 , {in 0 !}⟩ and ⟨𝛿 𝑧 , {out 1 ?}⟩, which indicates 𝛿 𝑥 = 𝛿 𝑧 . Therefore, their composition is illustrated in Fig. 9, which reflects the following result:

(init 𝑥 0 put * 𝑥 init 𝑎 0 ) ⊓ (init 𝑎 0 get * 𝑧 init 𝑥 0 ) (put 𝑥 ⊓ get 𝑧 ⊓ ode 01 ) * (17)
where

ode 01 = ⊢ ∼ 𝑥 0 = ∼ 𝑎 1 ∧ ∼ 𝑎 0 = ∼ 𝑧 1 ∧ ∼ 𝑧 1 = 0, {in 0 !, out 1 ?} If we ignore 𝜏s in traces, then (init 𝑥 0 put * 𝑥 init 𝑎 0 ) and (init 𝑎 0 get * 𝑧 init 𝑥 0 ) are equivalent to (init 𝑎 0 init 𝑥 0 put * 𝑥 )
and (init 𝑎 0 init 𝑥 0 get * 𝑧 ), respectively. Then, ( 17) can be simplified:

(init 𝑎 0 init 𝑥 0 put * 𝑥 ) ⊓ (init 𝑎 0 init 𝑥 0 get * 𝑧 ) (put 𝑥 ⊓ get 𝑧 ⊓ ode 01 ) * = init 𝑎 0 init 𝑥 0 (put * 𝑥 ⊓ get * 𝑧 ) (put 𝑥 ⊓ get 𝑧 ⊓ ode 01 ) * = init 𝑎 0 init 𝑥 0 (put 𝑥 ⊓ get 𝑧 ⊓ ode 01 ) * (18)
Note that the above result should be constrained by the healthiness condition of ( 13) which states 𝑎 0 and 𝑎 1 are aliases of 𝑎. Therefore, the above result is equivalent to [START_REF] Foster | Unifying Theories of Time with Generalised Reactive Processes[END_REF], which is equivalent to Plant of (15) (if 𝜏s are removed from traces). However, ( 16) is not equivalent to Plant HCSP HUTP , because the latter always terminates with put 𝑥 or get 𝑧 . Thus, the premise of the equivalence should be (1) 𝜙 0 : ignoring 𝜏s in traces and ( 2) 𝜙 1 : Plant terminates with put 𝑥 or get 𝑧 . In summary,

Plant ≡ 𝜙 0 ∧𝜙 1 Plant HCSP HUTP (19)
On the other hand, we study the conditions under which Control HCSP is consistent with Control of (11) under some conditions. Control HCSP can be translated as follows:

Control HCSP HUTP = ⊢ ⌈ti 0⌋ get 𝑥 comp 𝑦 comp 𝑧 put 𝑧 ⊢ ∼ 𝑥 1 = ∼ 𝑦 = ∼ 𝑧 0 = 0, ∅ 1 (get 𝑥 comp 𝑦 ) ◁ ti%2 = 0 ▷ skip HUTP (comp 𝑧 put 𝑧 ) ◁ ti%3 = 0 ▷ skip HUTP *
as illustrated by Fig. 10, where get 𝑥 = ⊢ ⌈ch 𝑥 ?, 𝑥 1 ⌋, put 𝑧 = ⊢ ⌈ch 𝑧 !, 𝑧 0 ⌋, comp 𝑦 = ⊢ ⌈𝑦 𝑥 1 + 1.5⌋ and comp 𝑧 = ⊢ ⌈𝑧 0 𝑦 × 2.4⌋. During the time intervals, the values of 𝑥 1 , 𝑦 and 𝑧 0 keep unchanged, denoted by the side condition on the left of the time line. Similarly, the behavior of Control in (11) can be illustrated by Fig. 11, where put 0 𝑦 = ⊢ ⌈out 0 !, 𝑦 0 ⌋, get 0 𝑦 = ⌈out 0 ?, 𝑦⌋, put 1 𝑦 = ⊢ ⌈in 1 !, 𝑦⌋ and get 1 𝑦 = ⊢ ⌈in 1 ?, 𝑦 1 ⌋. Compared to Fig. 10, the behaviour of Control is consistent with Control HCSP HUTP , except that the latter does not contain syn 0 𝑦 (synchronous communication between put 0 𝑦 and get 0 𝑦 ) and syn 1 𝑦 (synchronous communication between put 1 𝑦 and get 1 𝑦 ), because Control HCSP HUTP is a sequential process (and does not involve synchronous communication). This will lead to the inconsistency of the traces of Control HCSP HUTP and Control. In addition, the end time ti ′ of Control is not necessarily equal to the end time ti +𝑛 = 𝑛 of Control HCSP HUTP . Thus, the premise of the consistency should be (1) 𝜑 0 : ignoring trace variables and (2) 𝜑 1 : ti ′ %1 = 0. In summary,

Control ≡ 𝜑 0 ∧𝜑 1 Control HCSP HUTP (20)
Loop Note that the merge predicate 𝑀 𝐼 (Definition 4.5) allows the different termination time of parallel processes and it will delay the shorter one for the final time synchronisation. For example, Plant HCSP HUTP always terminate with put 𝑥 or get 𝑧 , while Control HCSP HUTP can terminate with

put 𝑧 ⊢ ∼ 𝑥 1 = ∼ 𝑦 = ∼ 𝑧 0 = 0, ∅ 1 skip HUTP skip HUTP .
For time synchronisation, 𝑀 {ch 𝑥 ,ch 𝑧 } will delay Plant HCSP HUTP for 1 time unit. In fact, the termination time difference raises when Control HCSP HUTP terminates with ti

′ %2 ≠ 0 ∧ ti ′ %3 ≠ 0. Thus, if ti ′ %2 = 0 ∨ ti ′ %3 = 0, ∥ HP 𝑀 {ch𝑥 ,ch𝑧 } will degrade into ∥ {ch 𝑥 ,ch 𝑧 } . Consider the condition 𝛾 : ti ′ %2 = 0 ∨ ti ′ %3 = 0, it implies 𝜑 1 ,
and furthermore, it implies 𝜙 1 because Control terminates with get 𝑥 or put 𝑧 under 𝛾, which indicates Plant will terminate with put 𝑥 or get 𝑧 . In a word, 𝛾 ⇒ 𝜙 1 ∧ 𝜑 1 . Additionally, it is known 𝜑 0 ⇒ 𝜙 0 .

Combining [START_REF] Gao | Delta-Decidability over the Reals[END_REF], [START_REF] Gao | dReal: An SMT Solver for Nonlinear Theories over the Reals[END_REF] and the monotonicity of ∥ {ch 𝑥 ,ch y } (Property 11),

Plant∥ {in 0 ,out 1 } Control ≡ 𝜑 0 ∧𝛾 Plant HCSP HUTP ∥ {ch 𝑥 ,ch 𝑧 } Control HCSP HUTP
given that in 0 and out 1 are aliases of ch 𝑥 and ch 𝑧 , respectively. In summary, we can conclude

RELATED WORK

Hoare and He's unifying theories of programming (UTP) [START_REF] Hoare | Unifying Theories of Programming[END_REF] is the first proposal towards unifying different programming paradigms and models under a common relational calculus suitable for design and verification. Another notable contribution in the same spirit is Milner's theory of bigraphs [START_REF] Milner | Pure Bigraphs: Structure and Dynamics[END_REF].

The concept of higher-order UTP dates back to [START_REF] Hoare | Unifying Theories of Programming[END_REF], where higher-order variables are introduced to represent predicates of methods and procedures. Based on [START_REF] Hoare | Unifying Theories of Programming[END_REF], Zeyda et al. propose a concept of higher-order UTP to set up a UTP theory for object-orientation [START_REF] Zeyda | Higher-Order UTP for a Theory of Methods[END_REF][START_REF] Zeyda | A Modular Theory of Object Orientation in Higher-Order UTP[END_REF]. [START_REF] Zeyda | Higher-Order UTP for a Theory of Methods[END_REF] builds a UTP theory for object-orientation by addressing four problems: consistency of the program model, redefinition of methods in subclasses, recursion and mutual recursion, and simplicity. [START_REF] Zeyda | A Modular Theory of Object Orientation in Higher-Order UTP[END_REF] supports recursion, dynamic binding, and compositional method definitions all at the same time. It shows how higherorder programming can be used to reason about object-oriented programs in a compositional manner and exemplifies its use by creating an object-oriented variant of a refinement language for real-time systems. In addition, it introduces the higher-order quantification over predicates. Unlike these higher-order extensions to UTP [START_REF] Hoare | Unifying Theories of Programming[END_REF][START_REF] Zeyda | Higher-Order UTP for a Theory of Methods[END_REF][START_REF] Zeyda | A Modular Theory of Object Orientation in Higher-Order UTP[END_REF], that presented in this paper focuses on higher-order quantification and the semantics of hybrid systems in the UTP theory.

Besides the de facto standards Simulink and Modelica, many more programming paradigms and domain-specific formalisms have been explored in the aim of modeling hybrid systems.

• Functional programming variants of data-flow concepts comprise Yampa [START_REF] Hudak | Arrows, Robots, and Functional Reactive Programming[END_REF], an extension of Haskell's functional reactive programming model (FRP, [START_REF] Peterson | Yale FRP User's Manual[END_REF]), or Zelus [START_REF] Bourke | Zélus: A Synchronous Language with ODEs[END_REF], a functional synchronous data-flow language to model ordinary differential equations in a so-called nonstandard time model. Like Modelica and Simulink, both lines of formalisms are devoted to simulation supporting type-based analysis of basic safety properties, such as causality. • Another line of work regards earlier attempts to extend rich process algebras like the 𝜋calculus with continuous real variables [START_REF] Bergstra | Process Algebra for Hybrid Systems[END_REF][START_REF] Cuijpers | Hybrid Process Algebra[END_REF][START_REF] Lanotte | A Calculus of Cyber-Physical Systems[END_REF]. These extensions lead to the corresponding formulations of bi-simulations as a foundation to verification.

Our approach is to define such an algebraically expressive formalism, yet devoted to the primary purpose of verifying hybrid system models, by embedding its definition, verification and proof capabilities in higher-order logic (Isabelle/HOL).

Hybrid automata [START_REF] Alur | Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems[END_REF] are a popular formalism to model hybrid systems, but composition/decomposition of automata results in an exponential blow up which is intractable analyze in practice. I/O hybrid automata [START_REF] Lynch | Hybrid I/O Automata[END_REF] is an extension of hybrid automata with explicit inputs and outputs. Assume-guarantee reasoning [START_REF] Henzinger | Assume-Guarantee Reasoning for Hierarchical Hybrid Systems[END_REF] on such automata tackles composability to prevent state-space explosion. However, their applicability is in practice restricted to linear hybrid automata.

Alternatively, proof-theoretic approaches to hybrid systems verification, such as differential dynamic logic (dL, [START_REF] Platzer | Differential Dynamic Logic for Hybrid Systems[END_REF][START_REF] Platzer | Logical Foundations of Cyber-Physical Systems[END_REF]), action systems [START_REF] Back | Generalizing Action Systems to Hybrid Systems[END_REF], hybrid Hoare logic together with hybrid communicating sequential processes (HHL/HCSP, [START_REF] He | From CSP to Hybrid Systems[END_REF][START_REF] Liu | A Calculus for Hybrid CSP[END_REF][START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams-A Deductive Approach[END_REF][START_REF] Zhou | A Formal Description of Hybrid Systems[END_REF]) and hybrid Event-B [START_REF] Abrial | Formalizing Hybrid Systems with Event-B[END_REF][START_REF] Dupont | Event-B Hybridation: A Proof and Refinement-based Framework for Modelling Hybrid Systems[END_REF], have gained much attention by offering powerful abstraction, refinement and proof mechanisms to scale hybrid system verification to practical use cases. Also note an early model of CPSs in the Coq proof assistant [START_REF] Malecha | Towards Foundational Verification of Cyber-Physical Systems[END_REF], which introduces a library VeriDrone, a foundational framework for reasoning about CPSs at all levels from high-level models to C code that implements the system. Empowered by the extension of SAT modulo-theory of real variables, implementing the seminal works on 𝛿-decidability of [START_REF] Gao | Delta-Decidability over the Reals[END_REF][START_REF] Gao | dReal: An SMT Solver for Nonlinear Theories over the Reals[END_REF] in tools like dReal and dReach, provers allow for the tactics-guided mechanized verification of logic models of hybrid systems. [START_REF] Mitsch | Modeling and Analyzing Hybrid Systems with Sphinx[END_REF] introduces a verification-driven engineering toolset S𝜑nx, which uses KeYmaera as hybrid verification tool, for modelling hybrid systems, exchanging and comparing models and proofs, and managing verification tasks. Differential dynamic logic (dL) [START_REF] Platzer | Differential Dynamic Logic for Hybrid Systems[END_REF][START_REF] Platzer | Logical Analysis of Hybrid Systems[END_REF] extends dynamic logic [START_REF] Pratt | Semantical Considerations on Floyd-Hoare Logic[END_REF] to hybrid systems by allowing modalities over hybrid programs that extend classical sequential programs with ordinary differential equations to model the continuous evolution of physical artifacts. In order to deal with more complex behaviour of hybrid systems, some variants of dL were established, e.g., stochastic differential dynamic logic [START_REF] Platzer | Logical Analysis of Hybrid Systems[END_REF] and differential game logic [START_REF] Platzer | Differential Game Logic[END_REF].

In [START_REF] Loos | Differential Refinement Logic[END_REF] Loos and Platzer propose a differential refinement logic to cope with refinement relations among different levels of abstraction for a given simple hybrid system. It remains an open problem whether the approach can apply to more complex hybrid system. In [START_REF] Rajhans | Supporting Heterogeneity in Cyber-Physical Systems Architectures[END_REF] the authors investigate how to apply dL to define architecture of CPSs. However, parallelism and communication are not considered in dL and its variants. Recent component-based verification methodologies developed in dL [START_REF] Müller | A Component-Based Approach to Hybrid Systems Safety Verification[END_REF][START_REF] Müller | Tactical Contract Composition for Hybrid System Component Verification[END_REF][START_REF] Ruchkin | Architecture Abstractions for Hybrid Programs[END_REF] propose composition operators in dL to split verification of systems into more manageable pieces. [START_REF] Lunel | Compositional Proofs in Differential Dynamic Logic dL[END_REF][START_REF] Lunel | Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic[END_REF] extend them with parallel composition (true concurrency) using design patterns defined using the primitive constructs of dL, which requires the corresponding mechanization effort as tactics in KeYmaeraX.

HCSP is a hybrid extension of Hoare's Communicating Sequential Processes [START_REF] Hoare | Communicating Sequential Processes[END_REF]. It features a native parallel composition operator and communicating primitives in addition to standard constructs for hybrid systems (sequences, loops, ODEs) and a proof calculus called hybrid Hoare logic (HHL) [START_REF] Liu | A Calculus for Hybrid CSP[END_REF], as well as several extensions for dealing with more complex behavious, e.g., fault-tolerance [START_REF] Wang | Modelling and Verifying Communication Failure of Hybrid Systems in HCSP[END_REF] and noise [START_REF] Wang | A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems[END_REF]. Also, the notion of approximate bisimulation was proposed in [START_REF] Yan | Automatically Generating SystemC Code from HCSP Formal Models[END_REF], with which a refinement relation between continuous models and between continuous models and discrete models can be well coped with. However, it is difficult to use HHL/HCSP to play a semantics foundation for the design of hybrid systems using MBD and DbC, as it is not easy to unify different models and views at different level of abstraction in HHL/HCSP.

Röonkkö and Ravn, and Back et al. extended action system [START_REF] Back | Refinement Calculus-A Systematic Introduction[END_REF] to hybrid systems, called hybrid action system [START_REF] Rönkkö | Action Systems with Continuous Behaviour[END_REF] and continuous action system [START_REF] Back | Generalizing Action Systems to Hybrid Systems[END_REF], respectively. As conservative extensions of action systems, theoretically speaking, both hybrid action system and continuous action system could support MBD and DbC. But both of them are very weak on dealing with continuous behaviours. In particular, they lack refinement relations, different continuous models and/or discrete models, which are essential for the MBD and DbC of hybrid systems.

CONCLUSIONS AND FUTURE WORKS

This paper defines a conservative extension to Hoare and He's UTP theory with higher-order quantification and provides a formal semantics for modeling and verifying hybrid systems, mixing discrete real-time processes and continuous dynamics. To this end, HUTP introduces real-time variables, denoted as functions over time, and allows the derivative of a variable to occur in a predicate, to define differential relations. This introduction allows to draw the concepts of hybrid processes and (normal) hybrid designs.

Our goal is to use the HUTP to define a formal semantics for engineering and formally verifying models such as Matlab's Simulink/Stateflow and/or the SAE's AADL, but also HCSP, and support the workflow of these environment with formal verification and certification functionalities inherited from its implementation in higher-order logic (Isabelle/HOL). We intend to additionally use HUTP to justify the correctness of the translation between these models and HCSP by translation validation as an appliaction of HUTP.

Future Works. Starting from the definition of normal hybrid design contracts presented in this paper, we are seeking principled abstractions to support modular analysis and compositional verification of hybrid system models. Our initial intuition was to start from the definition of abstract hybrid processes in Section 4.5 and define a theory of contracts using Abadi and Lamport's "composing specifications" [START_REF] Abadi | Composing Specifications[END_REF] or Benveniste's meta-theory of contracts [START_REF] Benveniste | Contracts for System Design[END_REF]. Indeed, consider a normal hybrid design HC ⊢ HP and H a HP -healthy abstract hybrid processes 𝐶 and 𝑃 such that HC ⊑ 𝐶 and 𝑃 ⊑ HP. The abstract design 𝐶 ⊢ 𝑃 naturally forms a contractual property of HC ⊢ HP, in the sense of Abadi and Lamport or Benveniste.

However, related works in the UTP [START_REF] Foster | Unifying Theories of Reactive Design Contracts[END_REF] show that the algebraic elaboration of such a contract theory requires non-constructive definitions such as weakest liberal preconditions and weakest rely, which prevent the structural decomposition and abstraction of parallel composition and communications from the abstracted hybrid designs (unless one uses, e.g., Lamport's encoding of hand-shake communications using shared variables).

As a result, our aim will instead be to elaborate a dependently-typed session calculus [START_REF] Majumdar | Multiparty Motion Coordination: From Choreographies to Robotics Programs[END_REF] in the UTP and equip it with abstract model checking capabilities [START_REF] Scalas | Verifying Message-Passing Programs with Dependent Behavioural Types[END_REF].

A PROOFS

A.1 Proofs for Timed Trace Model Property 1 (Associativity). Let 𝐼 0 , 𝐼 1 and 𝐼 2 be the respective common channel sets between timed traces tt 0 and tt 1 , tt 1 and tt 2 , and tt 2 and tt 0 , then

(tt 0 ∥ 𝐼 0 tt 1 ) ∥ 𝐼 1 ⊎𝐼 2 tt 2 = tt 0 ∥ 𝐼 0 ⊎𝐼 2 (tt 1 ∥ 𝐼 1 tt 2 ).
Proof. We prove by induction on the length of traces. Since the traces we consider could be infinite, the proof is coinductive. We start from the cases that |tt 0 |, |tt 1 |, |tt 2 | ≤ 1, such as tt 0 = tt 1 = tt 2 = 𝜖, then by the fact that 𝐼 0 , 𝐼 1 and 𝐼 2 are disjoint, we can get

(tt 0 ∥ 𝐼 0 tt 1 ) ∥ 𝐼 1 ⊎𝐼 2 tt 2 = tt 0 ∥ 𝐼 0 ⊎𝐼 2 (tt 1 ∥ 𝐼 1 tt 2 )
which indicates the associativity of the parallel composition of timed traces. □

A.2 Proofs for Hybrid Processes Theorem 4.2 (Idempotence and Monotonicity). H HP is idempotent and monotonic.

Proof. First, H HP is monotonic because it is constructed by monotonic operators. Then, we prove it is also idempotent. It can be checked that H 0 , H 1 , H 2 , H 3 and H 4 themselves are idempotent and H 0 and H 4 are commutative with their partners. Therefore,

H HP • H HP = (H 0 • H 1 • H 2 • H 3 • H 4 ) • (H 0 • H 1 • H 2 • H 3 • H 4 ) = (H 1 • H 2 • H 3 ) • (H 0 • H 0 • H 1 • H 2 • H 3 • H 4 • H 4 ) = (H 1 • H 2 • H 3 ) • (H 0 • H 1 • H 2 • H 3 • H 4 ) (21)
It is not difficult to check that H 3 is commutative with H 0 and H 1 , and we prove it is also commutative with H 2 . For short, let inf = (ti = +∞ ∨ |tr | = +∞) and inf ′ = (ti ′ = +∞ ∨ |tr ′ | = +∞) correspondingly. Let ♮ = (ti = ti ′ ∧ tr = tr ′ ). Then,

H 2 • H 3 (𝑋 ) = ♮ ◁ inf ▷ ((∃s ′ • 𝑋 ) ◁ inf ′ ▷ 𝑋 ) and H 3 • H 2 (𝑋 ) = (∃s ′ • (♮ ◁ inf ▷ 𝑋 )) ◁ inf ′ ▷ (♮ ◁ inf ▷ 𝑋 ) = (♮ ◁ inf ▷ ∃s ′ • 𝑋 ) ◁ inf ′ ▷ (♮ ◁ inf ▷ 𝑋 ) = ♮ ◁ inf ▷ (∃s ′ • 𝑋 ◁ inf ′ ▷ 𝑋 ) Therefore, H 2 • H 3 = H 3 • H 2 ,
and we can continue the equation ( 21):

H HP • H HP = (H 1 • H 2 • H 3 ) • (H 0 • H 1 • H 2 • H 3 • H 4 ) = H 0 • H 1 • H 2 • H 1 • H 2 • H 3 • H 3 • H 4 = H 0 • H 1 • H 2 • H 1 • H 2 • H 3 • H 4
Lastly, we prove the composition

H 1 • H 2 is idempotent. Concretely, H 1 • H 2 (𝑋 ) = H 1 (♮) ◁ inf ▷ H 1 (𝑋 )
Then,

H 1 • H 2 • H 1 • H 2 (𝑋 ) = H 1 (♮) ◁ inf ▷ H 1 (H 1 (♮) ◁ inf ▷ H 1 (𝑋 )) = H 1 (♮) ◁ inf ▷ (H 1 (♮) ◁ inf ▷ H 1 (𝑋 )) = H 1 (♮) ◁ inf ▷ H 1 (𝑋 ) = H 1 • H 2 (𝑋 )
In summary, Proof. It can be checked that H 4 is commutative with its partners, thus

H HP • H HP = H 0 • H 1 • H 2 • H
H HP (𝑋 ) = H 0 • H 1 • H 2 • H 3 • H 4 (𝑋 ) = H 0 • H 1 • H 4 • H 2 • H 3 (𝑋 ) = H 014 (♮ ◁ inf ▷ ((∃s ′ • 𝑋 ) ◁ inf ′ ▷ 𝑋 )) (22)
where

H 014 = H 0 • H 1 • H 4 .
Then, H HP (𝑋 ) ⊓ H HP (𝑌 ) and H HP (𝑋 ) ⊔ H HP (𝑌 ) are

H 014 (♮ ◁ inf ▷ ((∃s ′ • 𝑋 ∨ 𝑌 ) ◁ inf ′ ▷ (𝑋 ∨ 𝑌 ))) = H HP (𝑋 ∨ 𝑌 ) H 014 (♮ ◁ inf ▷ ((∃s ′ • 𝑋 ∧ 𝑌 ) ◁ inf ′ ▷ (𝑋 ∧ 𝑌 ))) = H HP (𝑋 ∧ 𝑌 )
Therefore, ⊓ and ⊔ are H HP -preserving.

□ Lemma A.1. H 014 (𝑋 ) H 014 (𝑌 ) = H 014 (𝑋 𝑌 ), where H 014 = H 0 • H 1 • H 4 .
Proof. The computation is performed as follows:

H 014 (𝑋 ) H 014 (𝑌 ) = 𝑋 ∧ lim(tr) = ti ≤ ti ′ = lim(tr ′ ) ∧ tr ≤ tr ′ ∧ RC ∧ SD 𝑌 ∧ lim(tr) = ti ≤ ti ′ = lim(tr ′ ) ∧ tr ≤ tr ′ ∧ RC ∧ SD = ∃ti * , s * , tr * • 𝑋 [ti * , s * , tr * /ti ′ , s ′ , tr ′ ] ∧ 𝑌 [ti * , s * , tr * /ti, s, tr] ∧ lim(tr) = ti ≤ ti * = lim(tr * ) ≤ ti ′ = lim(tr ′ ) ∧ tr ≤ tr * ≤ tr ′ ∧RC [ti * /ti ′ ] ∧ RC [ti * /ti] ∧ SD[ti * /ti ′ ] ∧ SD[ti * /ti] = (𝑋 𝑌 ) ∧ lim(tr) = ti ≤ ti ′ = lim(tr ′ ) ∧ tr ≤ tr ′ ∧ RC ∧ SD = H 014 (𝑋 𝑌 ) □ Property 3.
If HP 0 and HP 1 are H HP -healthy, then so is HP 0 HP 1 .

Proof. As stated in the proof of Property 2 (see [START_REF] He | From CSP to Hybrid Systems[END_REF]), a hybrid process H HP (𝑋 ) can be represented by H 014 (♮ ◁ inf ▷ (∃s ′ • 𝑋 ◁ inf ′ ▷ 𝑋 )). This form can be transformed into a matrix:

¬inf ′ inf ′ H 014 (𝑋 ∧ ¬inf ∧ ¬inf ′ ) H 014 (∃s ′ • 𝑋 ∧ ¬inf ∧ inf ′ ) ¬inf false H 014 (♮ ∧ inf ∧ inf ′ ) inf
Imagine and ∨ as matrix multiplication and addition, respectively, then H HP (𝑋 ) H HP (𝑌 ) is

H 014 (𝑋 ∧ ¬inf ∧ ¬inf ′ ) H 014 (𝑌 ∧ ¬inf ∧ ¬inf ′ ) H 014 (𝑋 ∧ ¬inf ∧ ¬inf ′ ) H 014 (∃s ′ • 𝑌 ∧ ¬inf ∧ inf ′ ) ∨H 014 (∃s ′ • 𝑋 ∧ ¬inf ∧ inf ′ ) H 014 (♮ ∧ inf ∧ inf ′ ) false H 014 (♮ ∧ inf ∧ inf ′ )
By Lemma A.1, it can be simplified to

H 014 ((𝑋 𝑌 ) ∧ ¬inf ∧ ¬inf ′ ) H 014 (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ∧ ¬inf ∧ inf ′ ) false H 014 (♮ ∧ inf ∧ inf ′ )
which is equivalent to

H 014 (♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ◁ inf ′ ▷ (𝑋 𝑌 ))) (23)
where takes precedence over ∨. The predicate ♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ◁ inf ′ ▷ (𝑋 𝑌 )) is H 2 -healthy, and we prove it is also H 3 -healthy.

H 3 (♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ◁ inf ′ ▷ (𝑋 𝑌 ))) = (♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ◁ inf ′ ▷ ∃s ′ • (𝑋 𝑌 ))) ◁inf ′ ▷ (♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ◁ inf ′ ▷ (𝑋 𝑌 )))
which can be simplified to

(♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ))) ◁ inf ′ ▷ (♮ ◁ inf ▷ (𝑋 𝑌 )), equivalent to ♮ ◁ inf ▷ (∃s ′ • (𝑋 𝑌 ∨ 𝑋 ) ◁ inf ′ ▷ (𝑋 𝑌 )) itself. Therefore, ( 23
) is H 0 • H 1 • H 4 • H 2 • H 3 -
𝑋 = 𝑋 skip where skip = H 2 (ti = ti ′ ∧ tr = tr ′ ∧ s = s ′ ).
Proof. With the aid of matrix representation, skip can be transformed into a matrix:

¬inf ′ inf ′ ♮ ∧ s = s ′ ∧ ¬inf ∧ ¬inf ′ false ¬inf false ♮ ∧ inf ∧ inf ′ inf
Then, 𝑋 skip can be computed as

𝑋 ∧ ¬inf ∧ ¬inf ′ 𝑋 ∧ ¬inf ∧ inf ′ 𝑋 ∧ inf ∧ ¬inf ′ 𝑋 ∧ inf ∧ inf ′ ♮ ∧ s = s ′ ∧ ¬inf ∧ ¬inf ′ false false ♮ ∧ inf ∧ inf ′
which can be simplified to

𝑋 ∧ ¬inf ∧ ¬inf ′ ∃s ′ • 𝑋 ∧ ¬inf ∧ inf ′ 𝑋 ∧ ¬inf ∧ ¬inf ′ ∃s ′ • 𝑋 ∧ ¬inf ∧ inf ′
The above is equivalent to Proof. We only prove the second item, and others can be proved similarly.

(∃s ′ • 𝑋 ) ◁ inf ′ ▷ 𝑋 , which denotes H 3 . □ Property 5 (Quantification). ∃ ∼ 𝑥 • (HP 0 HP 1 ) = (∃ ∼ 𝑥 • HP 0 ) (∃ ∼ 𝑥 • HP 1 ) ∀ ∼ 𝑥 • (HP 0 HP 1 ) ⊒ (∀ ∼ 𝑥 • HP 0 ) (∀ ∼ 𝑥 • HP 1 ) ∃ ∼ 𝑥 • (HP 0 ⊓ HP 1 ) = (∃ ∼ 𝑥 • HP 0 ) ⊓ (∃ ∼ 𝑥 • HP 1 ) ∀ ∼ 𝑥 • (HP 0 ⊓ HP 1 ) ⊒ (∀ ∼ 𝑥 • HP 0 ) ⊓ (∀ ∼ 𝑥 • HP 1 ) ∃ ∼ 𝑥 • (HP 0 ⊔ HP 1 ) ⊑ (∃ ∼ 𝑥 • HP 0 ) ⊔ (∃ ∼ 𝑥 • HP 1 ) ∀ ∼ 𝑥 • (HP 0 ⊔ HP 1 ) = (∀ ∼ 𝑥 • HP 0 ) ⊔ (∀ ∼ 𝑥 • HP 1 ) ¬ ≀ ∃ ∼ 𝑥 • HP = ∀ ∼ 𝑥 • ¬ ≀ HP ¬ ≀ ∀ ∼ 𝑥 • HP = ∃ ∼ 𝑥 • ¬ ≀
(∀ ∼ 𝑥 • HP 0 ) (∀ ∼ 𝑥 • HP 1 ) = {HP 0 [𝑓 0 , 𝑔 0 / ∼ 𝑥, ∼ 𝑥] | 𝑓 0 : [ti, ti ′ ) → D ∧ 𝑔 0 : (ti, ti ′ ) ⇀ D ∧ CON(𝑓 0 , 𝑔 0 , ti, ti ′ )} {HP 1 [𝑓 1 , 𝑔 1 / ∼ 𝑥, ∼ 𝑥] | 𝑓 1 : [ti, ti ′ ) → D ∧ 𝑔 1 : (ti, ti ′ ) ⇀ D ∧ CON(𝑓 1 , 𝑔 1 , ti, ti ′ )} = ∃ti * , s * , tr * • HP 0 [ti * , s * , tr * , 𝑓 0 , 𝑔 0 /ti ′ , s ′ , tr ′ , ∼ 𝑥, ∼ 𝑥] 𝑓 0 : [ti, ti ′ ) → D ∧ 𝑔 0 : (ti, ti ′ ) ⇀ D ∧ CON(𝑓 0 , 𝑔 0 , ti, ti ′ ) ∧ HP 1 [ti * , s * , tr * , 𝑓 1 , 𝑔 1 /ti ′ , s ′ , tr ′ , ∼ 𝑥, ∼ 𝑥] 𝑓 1 : [ti, ti ′ ) → D ∧ 𝑔 1 : (ti, ti ′ ) ⇀ D ∧ CON(𝑓 1 , 𝑔 1 , ti, ti ′ ) = ∃ti * , s * , tr * • HP 0 [ti * , s * , tr * , 𝑓 0 , 𝑔 0 /ti ′ , s ′ , tr ′ , ∼ 𝑥, ∼ 𝑥] ∧HP 1 [ti * , s * , tr * , 𝑓 1 , 𝑔 1 /ti, s, tr, ∼ 𝑥, ∼ 𝑥] 𝑓 0 : [ti, ti * ) → D ∧ 𝑔 0 : (ti, ti * ) ⇀ D∧ 𝑓 1 : [ti * , ti ′ ) → D ∧ 𝑔 1 : (ti, ti * ) ⇀ D∧ CON(𝑓 0 , 𝑔 0 , ti, ti * ) ∧ CON(𝑓 1 , 𝑔 1 , ti * , ti ′ ) = ∃ti * , s * , tr * • HP 0 [ti * , s * , tr * , 𝑓 0 , 𝑔 0 /ti ′ , s ′ , tr ′ , ∼ 𝑥, ∼ 𝑥] ∧HP 1 [ti * , s * , tr * , 𝑓 1 , 𝑔 1 /ti, s, tr, ∼ 𝑥, ∼ 𝑥] [𝑓 , 𝑔/ ∼ 𝑥, ∼ 𝑥] 𝑓 : [ti, ti ′ ) → D∧ 𝑔 : (ti, ti ′ ) ⇀ D∧ CON(𝑓 , 𝑔, ti, ti ′ ) ⊑ ∃ti * , s * , tr * • HP 0 [ti * , s * , tr * , 𝑓 0 , 𝑔 0 /ti ′ , s ′ , tr ′ , ∼ 𝑥, ∼ 𝑥] ∧HP 1 [ti * , s * , tr * , 𝑓 1 , 𝑔 1 /ti, s, tr, ∼ 𝑥, ∼ 𝑥] [𝑓 , 𝑔/ ∼ 𝑥, ∼ 𝑥] 𝑓 : [ti, ti ′ ) → D∧ 𝑔 : (ti, ti ′ ) ⇀ D∧ CON(𝑓 , 𝑔, ti, ti ′ ) = {(HP 0 HP 1 ) [𝑓 , 𝑔/ ∼ 𝑥, ∼ 𝑥] | 𝑓 : [ti, ti ′ ) → D ∧ 𝑔 : (ti, ti ′ ) ⇀ D ∧ CON(𝑓 , 𝑔, ti, ti ′ )} = ∀ ∼ 𝑥 • (HP 0 HP 1 )
where 𝑓 is the concatenation of 𝑓 0 and 𝑓 1 , 𝑔 is the concatenation of 𝑔 0 and 𝑔 1 , and Proof. These operators except ¬ ≀ are constructed by monotonic atom operators. □ Theorem 4.6 (Complete Lattice). Let HP be the image of H HP , i.e., it is the set of all hybrid processes, then it forms a complete lattice with top and bottom:

CON(𝑓 , 𝑔, ti, ti ′ ) = ∀𝑡 ∈ (ti, ti ′ ) • 𝑓 (𝑡 -) = 𝑔(𝑡 -) ∧ 𝑓 (𝑡 + ) = 𝑔(𝑡 + ) □ Property 6 (Well-Definedness). 𝑀 𝐼 is well-defined.
⊤ HP = HP = H HP (false) ⊥ HP = HP = H HP (true)
Proof. Since H HP is idempotent and monotonic by Theorem 4.2, the complete lattice can be proved directly by the properties of and . □ Theorem 4.11 (Miracle). ⊤ HP is the only miracle of hybrid processes.

Proof. As mentioned in the proof of Property 2 (see ( 22)), a hybrid process H HP (𝑋 ) can be unfolded as

H 014 (♮ ◁ inf ▷ ((∃s ′ • 𝑋 ) ◁ inf ′ ▷ 𝑋 )), where H 014 = H 0 • H 1 • H 4 . Then, H HP • MIR(𝑋 ) = H 014 (♮ ◁ inf ▷ ((∃s ′ • 𝑋 ∧ inf) ◁ inf ′ ▷ (𝑋 ∧ inf))) = H 014 (♮ ◁ inf ▷ (false ◁ inf ′ ▷ false)) = H 014 • H 2 • H 3 (false) = H HP (false)
which is equivalent to ⊤ HP . □ Property 8 (Left Zero of ). ⊤ HP HP = ⊤ HP for any hybrid process HP.

Proof. As mentioned in the proof (see ( 23)) of Property 3, ⊤ HP H HP (𝑋 ) is equivalent to

H HP (false) H HP (𝑋 ) = H 014 (♮ ◁ inf ▷ (∃s ′ • (false 𝑋 ∨ false) ◁ inf ′ ▷ (false 𝑋 )))
which can be simplified to H HP (false) = ⊤ HP . □ Property 9 (Zero of ∥ 𝑀 ). HP∥ 𝑀 ⊤ HP = ⊤ HP ∥ 𝑀 HP = ⊤ HP for any hybrid process HP.

Proof. As mentioned in the proof (see ( 22)) of Property 2, ⊤ HP can be unfolded as

H 014 (♮ ◁ inf ▷ false) = inf ∧ H 014 (♮)
Then, ⊤ HP,𝑋 = inf ∧ H 014 (♮) 𝑋 (note that inf has no primed variables). Therefore,

⊤ HP ∥ 𝑀 HP = H HP ⊤ HP,𝑋 ∧ HP 𝑌 ∧ II 𝑀 = H HP (inf ∧ (H 014 (♮) 𝑋 ∧ HP 𝑌 ∧ II 𝑀)) = H 0 • H 1 • H 4 • H 3 • H 2 (inf ∧ (H 014 (♮) 𝑋 ∧ HP 𝑌 ∧ II 𝑀))
where

II = ti = ti ′ ∧ s = s ′ ∧ tr = tr ′ . Notice that H 2 (inf ∧ (H 014 (♮) 𝑋 ∧ HP 𝑌 ∧ II 𝑀)) is ♮ ◁ inf ▷ (inf ∧ (H 014 (♮) 𝑋 ∧ HP 𝑌 ∧ II 𝑀)) = ♮ ◁ inf ▷ false = H 2 (false)
which means

⊤ HP ∥ 𝑀 HP = H 0 • H 1 • H 4 • H 3 • H 2 (false) = ⊤ HP .
Similarly, we can prove HP∥ 𝑀 ⊤ HP = ⊤ HP . □ Theorem 4.13 (Idempotence and Monotonicity). H a HP is idempotent and monotonic.

Proof. First, H a HP is monotonic as it is constructed by monotonic operators. Then, it can be proved that H a 0 , H a 2 , H a 3 and H 4 are idempotent and commutative with each other, thus

H a HP = H a 0 • H a 2 • H a 3 • H 4 is idempotent. □ A.
3 Proofs for Hybrid Designs Theorem 5.2 (Operations).

(

) (HC 0 ⊢ HP 0 ) ⊓ (HC 1 ⊢ HP 1 ) = (HC 0 ∧ HC 1 ) ⊢ (HP 0 ∨ HP 1 ) (2) (HC 0 ⊢ HP 0 ) ⊔ (HC 1 ⊢ HP 1 ) = (HC 0 ∨ HC 1 ) ⊢ ((HC 0 ⇒ ≀ HP 0 ) ∧ (HC 1 ⇒ ≀ HP 1 )) (3) (HC 0 ⊢ HP 0 ) (HC 1 ⊢ HP 1 ) = (HC 0 ∧ ¬ ≀ (HP 0 ¬ ≀ HC 1 )) ⊢ (HP 0 HP 1 ) 1
Proof. The matrix representations of HC 0 ⊢ HP 0 and HC 1 ⊢ HP 1 are respectively ⊥ HP ⊥ HP ¬ ≀ HC 0 HC 0 ⇒ ≀ HP 0 and

⊥ HP ⊥ HP ¬ ≀ HC 1 HC 1 ⇒ ≀ HP 1
Their meet (⊓, ∨) and join (⊔, ∧) can be computed component-wisely as

⊥ HP ∨ ⊥ HP ⊥ HP ∨ ⊥ HP ¬ ≀ HC 0 ∨ ¬ ≀ HC 1 (HC 0 ⇒ ≀ HP 0 )∨ (HC 1 ⇒ ≀ HP 1 ) = ⊥ HP ⊥ HP ¬ ≀ (HC 0 ∧ HC 1 ) (HC 0 ∧ HC 1 ) ⇒ ≀ (HP 0 ∨ HP 1 ) ⊥ HP ∧ ⊥ HP ⊥ HP ∧ ⊥ HP ¬ ≀ HC 0 ∧ ¬ ≀ HC 1 (HC 0 ⇒ ≀ HP 0 )∧ (HC 1 ⇒ ≀ HP 1 ) = ⊥ HP ⊥ HP ¬ ≀ (HC 0 ∨ HC 1 ) (HC 0 ⇒ ≀ HP 0 )∧ (HC 1 ⇒ ≀ HP 1 )
respectively, which are respectively equivalent to (HC 0 ∧ HC 1 ) ⊢ (HP 0 ∨ HP 1 ) and (HC 0 ∨ HC 1 ) ⊢ ((HC 0 ⇒ ≀ HP 0 ) ∧ (HC 1 ⇒ ≀ HP 1 ))

according to [START_REF] Abrial | Formalizing Hybrid Systems with Event-B[END_REF]. Imagine and ∨ as matrix multiplication and addition, respectively, then

⊥ HP ⊥ HP ¬ ≀ HC 0 HC 0 ⇒ ≀ HP 0 ⊥ HP ⊥ HP ¬ ≀ HC 1 HC 1 ⇒ ≀ HP 1 = (⊥ HP ⊥ HP ) ∨ (⊥ HP ¬ ≀ HC 1 ) (⊥ HP ⊥ HP ) ∨ (⊥ HP (HC 1 ⇒ ≀ HP 1 )) (¬ ≀ HC 0 ⊥ HP )∨ ((HC 0 ⇒ ≀ HP 0 ) ¬ ≀ HC 1 ) (¬ ≀ HC 0 ⊥ HP )∨ ((HC 0 ⇒ ≀ HP 0 ) (HC 1 ⇒ ≀ HP 1 )) = ⊥ HP ⊥ HP ¬ ≀ HC 0 ∨ (HP 0 ¬ ≀ HC 1 ) ¬ ≀ HC 0 ∨ (HP 0 ¬ ≀ HC 1 ) ∨ (HP 0 HP 1 ) = ⊥ HP ⊥ HP ¬ ≀ (HC 0 ∧ ¬ ≀ (HP 0 ¬ ≀ HC 1 )) (HC 0 ∧ ¬ ≀ (HP 0 ¬ ≀ HC 1 )) ⇒ ≀ (HP 0 HP 1 )
which is equivalent to (HC 0 ∧ ¬ ≀ (HP 0 ¬ ≀ HC 1 )) ⊢ (HP 0 HP 1 ) by [START_REF] Abrial | Formalizing Hybrid Systems with Event-B[END_REF]. □ Theorem 5.3 (Parallel Composition).

(HC 0 ⊢ HP 0 ) ∥ NHD(𝑀) (HC 1 ⊢ HP 1 ) = ¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∧¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∧¬ ≀ (¬ ≀ HC 1 ∥ ⊥ HP HP 0 ) ⊢ HP 0 ∥ 𝑀 HP 1
Proof. According to Section 4.2.5, (HC 0 ⊢ HP 0 ) ∥ NHD(𝑀) (HC 1 ⊢ HP 1 ) can be unfolded as

H HP ((HC 0 ⊢ HP 0 ) 𝑋 ∧ (HC 1 ⊢ HP 1 ) 𝑌 ∧ II NHD(𝑀)) (24)
where II = (ti = ti ′ ∧ s = s ′ ∧ tr = tr ′ ). With the aid of the matrix representation, the predicate (HC 0 ⊢ HP 0 ) 𝑋 ∧ (HC 1 ⊢ HP 1 ) 𝑌 ∧ II can be rewritten as Then, (HC 0 ⊢ HP 0 ) 𝑋 ∧ (HC 1 ⊢ HP 1 ) 𝑌 ∧ II NHD(𝑀), where ∧ takes precedence over , is equivalent to the following matrix, by treating and ∨ as matrix multiplication and addition, respectively. which can be simplified to H HP (𝑋 ⊥ HP ) according to [START_REF] He | From CSP to Hybrid Systems[END_REF]. □ Proof. We say the HUTP semantics and the structural operational semantics (SOS) of an HCSP process are consistent iff they keep consistent on time, state and trace. The proof for the consistency is divided into two stages: first, we prove the consistency between the SOS and the HUTP semantics of the syntactic entities in (3); then, we prove the semantics consistency for the operators, such as sequential and parallel compositions, which connect the syntactic entities. For brevity, we just show the key points of the proof in the following content.

¬ok ′ 𝑋 ∧ ¬ok ′ 𝑌 ok ′ 𝑋 ∧ ¬ok ′ 𝑌 ¬ok ′ 𝑋 ∧ ok ′ 𝑌 ok ′ 𝑋 ∧ ok ′ 𝑌 ⊥ 𝑋 HP ∧ ⊥ 𝑌 HP ∧ II ⊥ 𝑋 HP ∧ ⊥ 𝑌 HP ∧ II ⊥ 𝑋 HP ∧ ⊥ 𝑌 HP ∧ II ⊥ 𝑋 HP ∧ ⊥
The semantics consistency for ODE with communication interruption (ODE ⊵ ) has been proved in the end of Section 6.2. ODE ⊵ is representative because it covers the characteristic features of HCSP, such as continuous evolution, communication and interruption. The semantics consistency for other syntactic entities of HCSP like ⟨𝐹 ( s, s) = 0&𝐵⟩ and ch?𝑥 can be proved similarly. So, we only focus on proving the semantics consistency for the connector of parallel composition as it plays an important role in composite systems.

The SOS for parallel composition of HCSP processes is described by the following rules, where 𝐼 is the common channel set between parallel operands.

(𝜀 ∥𝜀, (ti, s 𝑃 ⊎ s 𝑄 )) → (𝜀, (ti, s 𝑃 ⊎ s 𝑄 ))

[Par0] (P, (ti, s 𝑃 ))

𝜏 -→ (P ′ , (ti, s ′ 𝑃 )) (P∥Q, (ti, s 𝑃 ⊎ s 𝑄 )) Since parallel HCSP processes do not share variables, the HUTP semantics and the SOS of the parallel connector are consistent on state variables naturally. Then, we focus on the parallel composition of timed traces, i.e., prove the consistency on timed traces. The above five rules correspond to the respective five composition rules of timed traces in Section 3. tt, we can prove that the parallel composition ∥ 𝐼 of timed traces in HUTP can be interpreted by the structural operational semantics of the parallel composition of HCSP. On the other side, we can prove that the SOS of the parallel composition of HCSP can also be interpreted by ∥ 𝐼 of timed traces in HUTP by induction on the derivation of (P∥Q, (ti, s 𝑃 ⊎ s 𝑄 ))

tt --→ * (𝜀, (ti ′ , s ′ 𝑃 ⊎ s ′ 𝑄 )) from the cases that |tt| ≤ 1. In summary, the SOS and the HUTP semantics of the parallel composition of HCSP are consistent on time, state and trace. The semantics consistency for other operators can be proved similarly. □

Example 3 . 3 .

 33 Consider an ordinary differential equation (ODE) with communication interruption:𝑥 1; ⟨ 𝑥 = 𝑥&true⟩ ⊵ (sensor!𝑥 → actuator?𝑥) ∥ wait 2; sensor?𝑦; actuator!(𝑦 + 1)

∼

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

  e., 𝛼 (∃𝑠 •HP) = 𝛼 (HP)\{𝑠}, 𝛼 (∃𝑠 ′ •HP) = 𝛼 (HP)\{𝑠 ′ } and 𝛼 (∃ ∼ 𝑠 •HP) = 𝛼 (HP)\{ ∼ 𝑠, ∼ 𝑠}. Dually, universal quantifications of 𝑠, 𝑠 ′ and ∼ 𝑠 can be defined by ∀𝑠 • HP = ¬ ≀ (∃𝑠 • ¬ ≀ HP) ∀𝑠 ′ • HP = ¬ ≀ (∃𝑠 ′ • ¬ ≀ HP) ∀ ∼ 𝑠 • HP = ¬ ≀ (∃ ∼ 𝑠 • ¬ ≀ HP) ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

Definition 4 . 5 (

 45 𝑀 𝐼 ). Let s 0 and s 1 be state variables (s 0 ∩ s 1 = ∅) owned by HP 0 and HP 1 , respectively, and 𝐼 a set of channels via which HP 0 and HP 1 communicate. Then, we define𝑀 𝐼 =syn mrg ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

  Definition 4.8 (Divergence). A divergence is a fixed point of 𝑋 = H HP • DIV (𝑋 ) where DIV (𝑋 ) = 𝑋 ∧ ti ′ < +∞ ∧ |tr ′ | = +∞ Definition 4.9 (Deadlock). A deadlock is a fixed point of 𝑋 = H HP • DL(𝑋 ) where

Definition 4 .

 4 10 (Miracle). A miracle is a fixed point of 𝑋 = H HP • MIR(𝑋 ) where MIR(𝑋 ) = 𝑋 ∧ (ti = +∞ ∨ |tr | = +∞) Theorem 4.11 (Miracle). ⊤ HP is the only miracle of hybrid processes. Miracle refines any hybrid process HP, i.e., HP ⊑ ⊤ HP , and it enjoys the following two desired properties, where Property 8 indicates miracle is non-terminated by Definition 4.7. Property 8 (Left Zero of ). ⊤ HP HP = ⊤ HP for any hybrid process HP. Property 9 (Zero of ∥ 𝑀 ). HP∥ 𝑀 ⊤ HP = ⊤ HP ∥ 𝑀 HP = ⊤ HP for any hybrid process HP.

Theorem 5 . 3 (

 53 Parallel Composition).

Theorem 5 . 5 (Theorem 5 . 6 (

 5556 Closure). Normal hybrid designs are closed on ⊓, ⊔, , ∥ NHD(𝑀) and ∥ HP 𝑀 . Refinement). (HC 0 ⊢ HP 0 ) ⊑ (HC 1 ⊢ HP 1 ) iff HC 1 ⊑ HC 0 and HP 0 ⊑ (HC 0 ∧ HP 1 )

Theorem 5 . 7 (

 57 Complete Lattice). Normal hybrid designs form a complete lattice with top ⊤ NHD = ⊥ HP ⊢ ⊤ HP and bottom ⊥ NHD = ⊤ HP ⊢ ⊥ HP Property 12 (Chaos). ⊥ NHD = ⊤ HP ⊢ HP for any hybrid process HP. Property 13 (Non-termination). For any normal hybrid design NHD, ⊥ NHD NHD = ⊥ NHD and ⊤ NHD NHD = ⊤ NHD Property 14 (Parallel Composition). For any normal hybrid design NHD, NHD∥ NHD(𝑀) ⊤ NHD = ⊤ NHD ∥ NHD(𝑀) NHD = ⊤ NHD Property 15 (Parallel Composition). For any normal hybrid design NHD, NHD∥ HP 𝑀 ⊥ NHD = ⊥ NHD ∥ HP 𝑀 NHD = ⊥ NHD The above conclusions demonstrate that the chaos ⊥ NHD of normal hybrid designs enjoys the desired properties that (1) it is non-terminated (left-zero of sequential composition, see Property 13) and (

6. 3 . 2 Fig. 4 .

 324 Fig. 4. Continuous blocks

Fig. 5 .

 5 Fig. 5. Continuous Math Operation Block with D/A and A/D converters

𝑦 1

 1 satisfy the expected assumptions during the whole course of action then, the value of ∼ 𝑧 0 is, at all times, equal to the result of the operation of ∼ 𝑥 and ∼ 𝑦 1 in time.

Fig. 8 .Fig. 9 .

 89 Fig. 8. FSMs of traces of init 𝑥 0 (put 𝑥 ⊓ ode 0 ) * (left) and init 𝑎 0 (get 𝑧 ⊓ ode 1 ) * (right)

Loop

Fig. 10 .

 10 Fig. 10. Visual representation of HUTP semantics of Control HCSP

Fig. 11 .

 11 Fig. 11. Visual representation HUTP semantics of Control

Diagram

  HUTP ≡ 𝑇 ,𝑆 Diagram HCSP HUTP where 𝑇 = {𝑡 ≥ 0 | 𝑡%2 = 0 ∨ 𝑡%3 = 0} and 𝑆 = {𝑥 0 , 𝑥 1 , 𝑦, 𝑧 0 , 𝑧 1 , 𝑎 0 , 𝑎 1 }. ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

  HP ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

  Proof. The conditions (1) and (2) of well-definedness of 𝑀 𝐼 hold by its definition. We prove the condition (3) also holds for 𝑀 𝐼 . First, if |tr 𝑋 | < +∞ and |tr 𝑌 | < +∞, by the definition of ∥ 𝐼 , |tr ′ | < +∞. Then, if |tr 𝑋 | = +∞ or |tr 𝑌 | = +∞, say |tr 𝑋 | = +∞, there are two cases: (a) |tr | = +∞, since tr ≤ tr ′ by H 0 , |tr ′ | = +∞; (b) |tr | < +∞, meaning |tr 𝑋 -tr | = +∞. According to the definition of ∥ 𝐼 , the composed trace is not shorter than the individual traces, i.e., |tr ′ -tr | ≥ |tr 𝑋 -tr | = +∞, implying |tr ′ | = +∞. Therefore, the condition (3) holds, indicating 𝑀 𝐼 is well-defined. □ Property 7 (Monotonicity). The operators , ⊔, ⊓, ◁▷, ∃ and ∥ 𝑀 are monotonic and ¬ ≀ is anti-monotone, with respect to the refinement order ⊑.

  HC 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP ∨ (¬ ≀ HC 0 ) 𝑋 ∧ (HC 1 ⇒ ≀ HP 1 ) 𝑌 ∧ II ⊥ HP ∨(HC 0 ⇒ HP 0) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP (¬ ≀ HC 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP ∨ (¬ ≀ HC 0 ) 𝑋 ∧ (HC 1 ⇒ ≀ HP 1 ) 𝑌 ∧ II ⊥ HP ∨ (HC 0 ⇒ HP 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP ∨ (HC 0 ⇒ HP 0 ) 𝑋 ∧ (¬ ≀ HC 1 ⇒ ≀ HP 1 ) 𝑌 ∧ II 𝑀 okThis matrix can be simplified as follows:¬ok ′ ok ′ ⊥ HP ⊥ HP ¬ok (¬ ≀ HC 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP ∨(¬ ≀ HC 0 ) 𝑋 ∧ (HP 1 ) 𝑌 ∧ II ⊥ HP ∨(HP 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP (¬ ≀ HC 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP ∨(¬ ≀ HC 0 ) 𝑋 ∧ (HP 1 ) 𝑌 ∧ II ⊥ HP ∨(HP 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II ⊥ HP ∨(HP 0 ) 𝑋 ∧ (HP 1 ) 𝑌 ∧ II 𝑀 okTherefore, the hybrid process of (24) is equivalent to the following matrix:¬ok ′ ok ′ ⊥ HP ⊥ HP ¬ok (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∨ (HP 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∨(¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) (¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∨ (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∨(HP 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∨ (HP 0 ∥ 𝑀 HP 1 ) ok which is equivalent to ¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∨ (HP 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∨(¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC1 ) ⊢ (HP 0 ∥ 𝑀 HP 1 ) by the matrix representation of hybrid designs (see (2)). □ Lemma A.2. H HP (𝑋 ) ⊥ HP = H HP (𝑋 ⊥ HP ). Proof. As mentioned in the proof (see (23)) of Property 3, H HP (𝑋 ) ⊥ HP is equivalent to H HP (𝑋 ) H HP (⊥ HP ) = H 014 (♮ ◁ inf ▷ (∃s ′ • (𝑋 ⊥ HP ∨ 𝑋 ) ◁ inf ′ ▷ 𝑋 ⊥ HP ))

Theorem 5 . 5 (

 55 Closure). Normal hybrid designs are closed on ⊓, ⊔, , ∥ NHD(𝑀) and ∥ HP 𝑀 .Proof. We only prove the closure of normal hybrid designs on ∥ NHD(𝑀) . The key is to prove Assumption = ¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∧ ¬ ≀ (HP 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∧ ¬ ≀ (¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) is H HC -healthy, i.e., ¬ ≀ Assumption ⊥ HP = ¬ ≀ Assumption. Concretely,¬ ≀ Assumption ⊥ HP = (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ∨ (HP 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ∨ (¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ⊥ HP By Lemma A.2, (¬ ≀ HC 0 ∥ ⊥ HP HP 1 ) ⊥ HP is equivalent to H HP (¬ ≀ HC 𝑋 0 ∧ HP 𝑌 1 ∧ II ⊥ HP ) ⊥ HP = H HP (¬ ≀ HC 𝑋 0 ∧ HP 𝑌 1 ∧ II ⊥ HP ⊥ HP ) = H HP (¬ ≀ HC 𝑋 0 ∧ HP 𝑌 1 ∧ II ⊥ HP ) = ¬ ≀ HC 0 ∥ ⊥ HP HP 1Similarly, we can prove that (HP 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ⊥ HP and (¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 ) ⊥ HP are equivalent to HP 0 ∥ ⊥ HP ¬ ≀ HC 1 and ¬ ≀ HC 0 ∥ ⊥ HP ¬ ≀ HC 1 , respectively. Thus, ¬ ≀ Assumption ⊥ HP = ¬ ≀ Assumption, i.e., Assumption is H HC -healthy. □ Lemma A.3. HP 0 ⊑ HP 1 iff HP 0 ⊓ ¬ ≀ HP 1 = ⊥ HP for HP 0 and HP 1 are hybrid processes.Proof.HP 0 ⊑ HP 1 iff ¬ ≀ HP 1 ⊑ ¬ ≀ HP 0 iff ⊥ HP ⊑ (HP 0 ⊓ ¬ ≀ HP 1 ) ⊑ (HP 0 ⊓ ¬ ≀ HP 0 ) = ⊥ HPaccording to the monotonicity of ⊓ (Property 7). □ Theorem 5.6 (Refinement). (HC 0 ⊢ HP 0 ) ⊑ (HC 1 ⊢ HP 1 ) iffHC 1 ⊑ HC 0 and HP 0 ⊑ (HC 0 ∧ HP 1 )Proof. According to the matrix representation, (HC 0 ⊢ HP 0 ) ⊑ (HC 1 ⊢ HP 1 ) iff⊥ HP ⊥ HP ¬ ≀ HC 0 HC 0 ⇒ ≀ HP 0 ⊑ ⊥ HP ⊥ HP ¬ ≀ HC 1 HC 1 ⇒ ≀ HP 1 iff ¬ ≀ HC 0 ⊑ ¬ ≀ HC 1 and (HC 0 ⇒ ≀ HP 0 ) ⊑ (HC 1 ⇒ ≀ HP 1 ). Then, ⊥ HP = (HC 0 ⇒ ≀ HP 0 ) ⊓ ¬ ≀ (HC 1 ⇒ ≀ HP 1 ) [Lemma A.3] = ¬ ≀ HC 0 ⊓ HP 0 ⊓ (HC 1 ⊔ ¬ ≀ HP 1 ) = ¬ ≀ HC 0 ⊓ HP 0 ⊓ ¬ ≀ HP 1 [¬ ≀ HC 0 ⊑ ¬ ≀ HC 1 and Lemma A.3]Applying Lemma A.3 again, the above result is equivalent toHP 0 ⊑ ¬ ≀ (¬ ≀ HC 0 ⊓ ¬ ≀ HP 1 ) ≡ (HC 0 ∧ HP 1 )□ Property 10 (Contra-variance). If HC 0 ⊒ HC 1 and HP 0 ⊑ HP 1 then(HC 0 ⊢ HP 0 ) ⊑ (HC 1 ⊢ HP 1 )Proof. It can be proved directly from Theorem 5.6. □ Property 11 (Monotonicity). Operators ⊔, ⊓, , ∥ NHD(𝑀) and ∥ HP 𝑀 for normal hybrid designs are monotonic with respect to ⊑.Proof. These operators are constructed from monotonic atomic operators. □ Theorem 5.7 (Complete Lattice). Normal hybrid designs from a complete lattice with top ⊤ NHD = ⊥ HP ⊢ ⊤ HP and bottom ⊥ NHD = ⊤ HP ⊢ ⊥ HP Proof. According to Theorem 5.2, ⊓ and ⊔ can be generalised to 𝑖 (HC 𝑖 ⊢ HP 𝑖 ) = ( 𝑖 HC 𝑖 ) ⊢ ( 𝑖 HP 𝑖 ) 𝑖 (HC 𝑖 ⊢ HP 𝑖 ) = ( 𝑖 HC 𝑖 ) ⊢ ( 𝑖 (HC 𝑖 ⇒ ≀ HP 𝑖 )) Therefore, normal hybrid designs form a complete lattice under ⊑ with ⊤ NHD = ⊥ HP ⊢ ⊤ HP ⊥ NHD = ⊤ HP ⊢ ⊥ HP □ Property 12 (Chaos). ⊥ NHD = ⊤ HP ⊢ HP for any hybrid process HP. Proof. By the matrix representation, ⊤ HP ⊢ HP = ⊥ HP ⊥ HP ¬ ≀ ⊤ HP ⊤ HP ⇒ ≀ HP = ⊥ HP ⊥ HP ⊥ HP ⊥ HP = ⊥ NHD □ Property 13 (Non-termination). For any normal hybrid design NHD, ⊥ NHD NHD = ⊥ NHD and ⊤ NHD NHD = ⊤ NHD Proof. Let NHD = HC ⊢ HP. By matrix representations, ⊥ NHD NHD = ⊥ HP ⊥ HP ⊥ HP ⊥ HP ⊥ HP ⊥ HP ¬ ≀ HC HC ⇒ ≀ HP = ⊥ HP ⊥ HP ⊥ HP ⊥ HP = ⊥ NHD ⊤ NHD NHD = ⊥ HP ⊥ HP ⊤ HP ⊤ HP ⊥ HP ⊥ HP ¬ ≀ HC HC ⇒ ≀ HP = ⊥ HP ⊥ HP ⊤ HP ⊤ HP = ⊤ NHD □ Property 14 (Parallel Composition). For any normal hybrid design NHD, NHD∥ NHD(𝑀) ⊤ NHD = ⊤ NHD ∥ NHD(𝑀) NHD = ⊤ NHD Proof. It can be proved by Property 9 and Theorem 5.3. □ Property 15 (Parallel Composition). For any normal hybrid design NHD, NHD∥ HP 𝑀 ⊥ NHD = ⊥ NHD ∥ HP 𝑀 NHD = ⊥ NHD Proof. Let NHD = HC ⊢ HP, then by Definition 5.4 and Property 12 we can get ⊥ NHD ∥ 𝑀 NHD = (⊤ HP ⊢ ⊥ HP ) ∥ 𝑀 (HC ⊢ HP) = ⊤ HP ⊢ (⊥ HP ∥ 𝑀 HP) = ⊥ NHD Similarly, we can prove NHD∥ 𝑀 ⊥ NHD = ⊥ NHD . □ A.4 Proofs for Reflection of HCSP and Simulink with HUTP Property 16 (Unit). ⌈⌋ is a unit of hybrid processes w.r.t. . Proof. According to the intermediate result (23) from Property 3, H HP (𝑋 ) ⌈⌋ = H HP (𝑋 ) H HP (ti = ti ′ < +∞ ∧ s = s ′ ∧ tr = tr ′ ) = H 014 (♮ ◁ inf ▷ ((∃s ′ • 𝑋 ) ◁ inf ′ ▷ 𝑋 )) = H HP (𝑋 ) by the intermediate result (22) from Property 2. Similarly, we can prove ⌈⌋ H HP (𝑋 ) = H HP (𝑋 ). □ Corollary 1 (Unit). ⊢ ⌈⌋ is a unit of hybrid processes w.r.t. . Proof. According to Property 16 and Theorem 5.2(3), for any normal hybrid design HC ⊢ HP, (⊢ ⌈⌋) (HC ⊢ HP) = (⊥ HP ∧ ¬ ≀ ( ⌈⌋ ¬ ≀ HC)) ⊢ ( ⌈⌋ HP) = HC ⊢ HP (HC ⊢ HP) (⊢ ⌈⌋) = (HC ∧ ¬ ≀ (HP ¬ ≀ ⊥ HP )) ⊢ (HP ⌈⌋) = HC ⊢ HP □ Theorem 6.1 (Semantics Consistency). The HUTP semantics of HCSP is consistent with the operational semantics of HCSP.

  ′ ∥Q, (ti, s ′ 𝑃 ⊎ s 𝑄 )) [Par1] ch ∈ 𝐼 (P, s 𝑃 ) ⟨ch?,𝑑 ⟩ -----→ (P ′ , s ′ 𝑃 ) (Q, s 𝑄 ) ⟨ch!,𝑑 ⟩ -----→ (Q ′ , s ′ 𝑄 ) (P∥Q, s 𝑃 ⊎ s 𝑄 ) ⟨ch,𝑑 ⟩ ----→ (P ′ ∥Q ′ , s ′ 𝑃 ⊎ s ′ 𝑄 ) [Par2] ch ∉ 𝐼 (P, (ti, s 𝑃 )) ⟨ch * ,𝑑 ⟩ -----→ (P ′ , (ti, s ′ 𝑃 )) (P∥Q, s 𝑃 ⊎ s 𝑄 ) ⟨ch * ,𝑑 ⟩ -----→ (P ′ ∥Q, s ′ 𝑃 ⊎ s 𝑄 ) [Par3] (P, (ti, s 𝑃 )) ⟨ti ′ -ti,RS 𝑃 ⟩ --------→ (P ′ , (ti ′ , s ′ 𝑃 ), ∼ s 𝑃 ) (Q, (ti, s 𝑄 )) ⟨ti ′ -ti,RS 𝑄 ⟩ ---------→ (Q ′ , (ti ′ , s ′ 𝑄 ), ∼ s 𝑄 ) RS 𝑃 ∩ RS 𝑄 = ∅ (P∥Q, (ti, s 𝑃 ⊎ s 𝑄 )) ⟨ti ′ -ti,RS 𝑃 ⊎RS 𝑄 ⟩ -------------→ (P ′ ∥Q ′ , (ti ′ , s ′ 𝑃 ⊎ s ′ 𝑄 ), ∼ s 𝑃 ⊎ ∼ s 𝑄 ) [Par4]

s

  3. Concretely, [Par0], [Par1], [Par2], [Par3] and [Par4] relate to [Empty], [𝜏-Act], [SynIO], [NoSynIO] and [SynWait], respectively. Consider two HCSP processes P and Q with respective states s 𝑃 and s 𝑄 . Their execution histories are recorded by timed traces tt 𝑃 and tt 𝑄 , respectively, denoted by (P, (ti, s 𝑃 )) tt 𝑃 ---→ * (𝜀, (ti ′ , s ′ 𝑃 ), ∼ s 𝑃 ) and (Q, (ti, s 𝑄 )) 𝑄 can be removed if there is no flow generated. The proof is by induction because all the traces involved are finite in the semantics of HCSP. So, this proceeds by induction on the length of traces and start from cases that |tt 𝑃 |, |tt 𝑄 | ≤ 1, such as tt 𝑃 = tt 𝑄 = 𝜖 or tt 𝑃 and tt 𝑄 are just trace blocks. Then, by induction on the derivation of tt 𝑃 ∥ 𝐼 tt 𝑄

  lim(tr ′ ) ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

•

  If the preceding process does not terminate, i.e., ti = +∞ ∨ |tr | = +∞, the current process should do nothing but keep the time and trace observations unchanged, i.e., H 2

  • If the current process does not terminate, i.e., ti ′ = +∞ ∨ |tr ′ | = +∞, the values of the output state variables are unobservable, i.e.,H 3 (𝑋 ) = (∃s ′ • 𝑋 ) ◁ (ti ′ = +∞ ∨ |tr ′ | = +∞) ▷ 𝑋As stated above, ti ′ = +∞ ∨ |tr ′ | = +∞ specify variable wait ′ in the traditional definition of reactive processes of the UTP, where wait ′ being true denotes the observation that all primed variables stand for intermediate observations, not final ones. However, in our work, we hide the primed state variables by an existential quantifier when ti ′ = +∞ ∨ |tr ′ | = +∞, since observing the state values at time infinity makes no sense. The idea of H 3 is similar to R4 for a healthy process in[START_REF] Butterfield | State Visibility and Communication in Unifying Theories of Programming[END_REF], which expresses the intuition that "program variable state is not visible while waiting for external events". • If the process evolves for a period of time, i.e., ti < ti ′ , the real-time value

	∼ s should keep
	right-continuous and semi-differentiable, i.e.,
	H 4

  H 2 and H 3 in Definition 4.1, respectively. A predicate is an abstract hybrid process iff it is H a HP -healthy. Compared with Definition 4.1 of H HP , abstract hybrid processes only consider time (ti and ti ′ ) and state (s, ′ ), ignoring the timed trace (tr and tr ′ ). Therefore, H 1 is no longer necessary here. By Theorem 4.13, abstract hybrid processes can form a complete lattice with top and bottom

	For brevity, we use H a HP to denote H a 0 • H a 2 • H a 3 • H 4 .
	Theorem 4.13 (Idempotence and Monotonicity). H a HP is idempotent and monotonic.
	Note that H a 0 , H a 2 and H a 3 are abstract versions of H 0 , ∼ s,

∼

s and s

  • ⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑖 ∈𝐼 (io i → P 𝑖 ) behaves like ⟨𝐹 ( s, s) = 0&𝐵⟩, except that the continuous evolution is preempted as soon as one of the communications io i takes place, which is followed by the respective P 𝑖 , where 𝑖𝑜 𝑖 stands for a communication event, i.e., either ch?x or ch!e.Notice that if the continuous part terminates before a communication among {io 𝑖 | 𝑖 ∈ 𝐼 } occurs, then the process terminates without communicating. Concretely,⟨𝐹 ( s, s) = 0&𝐵⟩ ⊵ 𝑖 ∈𝐼 (io i → P 𝑖 ) HUTP = exit ⊓ comm ⊓ (ode RS (exit ⊓ comm))(4)Without loss of generality, we let 𝐼 = 𝐼 ? ∪ 𝐼 ! with 𝐼 ? ∩ 𝐼 ! = ∅ such that io i = ch i ?x i if 𝑖 ∈ 𝐼 ? and ch i !e i otherwise (𝑖 ∈ 𝐼 ! ), where 𝑒 𝑖 is an arithmetic expression. Note that 𝑥 𝑖 and 𝑥 𝑗 can denote the same variable even if 𝑖 ≠ 𝑗. Let RS = {ch i ?, ch j ! | 𝑖 ∈ 𝐼 ? , 𝑗 ∈ 𝐼 ! } be the set of waiting channel operations. Then, the preemption by communication can be described by comm = input ⊓ output

	where
	input =	𝑖 ∈𝐼

? (⊢ ⌈ch i ?, 𝑥 𝑖 ⌋ P 𝑖 HUTP ) output = 𝑗 ∈𝐼 ! (E(𝑒 𝑗 (s)) ⊢ ⌈ch j !, 𝑒 𝑗 (s)⌋ P 𝑗 HUTP )

  [START_REF] Alur | Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems[END_REF] • H 4 = H HP , i.e., it is idempotent. □ Property 2. If HP 0 and HP 1 are H HP -healthy, HP 0 ⊓ HP 1 and HP 0 ⊔ HP 1 are H HP -healthy.

  healthy, i.e., H HP (𝑋 ) H HP (𝑌 ) is H HP -healthy. □ Property 4. The healthiness condition H 3 is equivalent to

  𝑌 HP ∧ II ¬ok (¬ ≀ HC 0 ) 𝑋 ∧ (¬ ≀ HC 1 ) 𝑌 ∧ II (¬ ≀ HC 0 ) 𝑋 ∧ II∧ (HC 1 ⇒ ≀ HP 1 ) 𝑌 (¬ ≀ HC 1 ) 𝑌 ∧ II∧ (HC 0 ⇒ ≀ HP 0 ) 𝑋 (HC 0 ⇒ ≀ HP 0 ) 𝑋 ∧ II ∧(HC 1 ⇒ ≀ HP 1 ) 𝑌 okSimilarly, NHD(𝑀) can also be represented by the transpose of the following matrix:NHD(𝑀) T = ¬ok 𝑋 ∧ ¬ok 𝑌 ok 𝑋 ∧ ¬ok 𝑌 ¬ok 𝑋 ∧ ok 𝑌 ok 𝑋 ∧ ok 𝑌

	⊥ HP	⊥ HP	⊥ HP	⊤ HP	¬ok ′
	⊥ HP	⊥ HP	⊥ HP	𝑀	ok ′

ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

https://gitee.com/bhzhan/mars.git ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: January 2022.

ACKNOWLEDGMENTS

This research is partly supported by NSFC under grant No. 62192732, 61625206, 62032024, 61972385 and 61732001, 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.