Guillaume Dupont
email: guillaume.dupont@enseeiht.fr

Yamine Ait-Ameur
email: yamine@enseeiht.fr

Neeraj Kumar Singh
email: neeraj.singh@enseeiht.fr

Marc Pantel
email: marc.pantel@enseeiht.fr

Formally Verified Architectural Patterns of Hybrid Systems Using Proof and Refinement with Event-B 1

Cyber-Physical Systems (CPSs) are multi-component systems that interact with the real world. Their heterogeneous nature makes them particularly difficult to model and prove.

Our work proposes a framework allowing to design complex hybrid systems based on decomposition using formally verified architectural patterns. It relies on a proof and refinement-based, correct-by-construction approach with Event-B. In particular, the generic model developed in our previous work is used as a base for defining different patterns, for modelling different architectures of systems.

Three architectural patterns are presented, corresponding to simple, centralised and distributed control: one controller controlling one plant, one controller controlling several plants and several controllers controlling several plants.

The progressive development of the proposed patterns and their application to specific hybrid systems allows to prove the required safety properties by introducing invariants, decomposing and balancing the proof effort at every step of the development. An assessment of the proposed architectural patterns is undertaken: different designs of the same case study are used to demonstrate the feasibility, reliability and extensibility of our approach to model and designing different classes of controllers.

Introduction

Hybrid systems integrate discrete and continuous behaviours at the same level. The formal development of hybrid systems has attracted the attention of several researchers in the field of formal verification, on the one hand, and control theory, on the other. These two types of research work contributed to define modelling and verification techniques for designing robust hybrid systems by ensuring the relevant properties guaranteeing safe hybrid systems behaviour. The work on formal verification has contributed to the proposal of formal modelling and verification techniques, borrowed from computer science models, enabling to reason on this type of systems and establishing their relevant properties, while control theory is interested in formal modelling based on differential equations to express and guarantee the properties of stability, approximation, linearisation, etc. The challenge is to offer to hybrid systems designers a framework and tools allowing to reason on both discrete and continuous behaviour.

The formal verification approaches integrate modelling and verification techniques from both fields of study. An example is the hybrid automation [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF] that integrates the notion of state-transition systems with state variables characterised by differential equations. The nature of these equations (linear or non-linear) influences the verification procedure by hybrid model checking. Another example concerns the hybrid programs of [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF], which extend dynamic logic with the possibility of handling state variables also characterised by differential equations. The definition of differential invariants and the use of equation solvers are introduced. These two examples clearly illustrate the successful integration of these two fields.

In addition, the same techniques are also interesting for modelling commonly used controllers, such as PIDs [START_REF] Aréchiga | Using theorem provers to guarantee closed-loop system properties[END_REF], the techniques of resolution and discretisation of differential equations [START_REF] Scherer | Discretization of Differential Equations[END_REF]. They rely on the definition of generic models that can be instantiated for the design and verification of specific hybrid systems.

There exist several approaches integrating continuous features in a pre-existing formal method. For instance, Hybrid Event-B [START_REF] Banach | Core Hybrid Event-B I: Single Hybrid Event-B machines[END_REF] extends Event-B's language, semantics and method as to define continuous behaviour (so-called pliant events), closely woven with discrete events (mode events). Continuous dynamics are modelled by functions of time, and can be expressed using differential equations.

Other examples of such approach include Hybrid CSP [START_REF] Liu | A calculus for hybrid CSP[END_REF], an hybridation of Hoare's Communicating Sequential Processes [START_REF] Hoare | Communicating Sequential Processes[END_REF], and Continuous Action System [START_REF] Back | Generalizing action systems to hybrid systems[END_REF], a continuous extension of Back's Action Systems [START_REF] Back | Decentralization of process nets with centralized control[END_REF].

Note that the presented approaches rely on modelling systems and performing proofs on models; so-called bottomup approaches consist in working directly with the controller's code (e.g. written in C) and to annotate it in order to incorporate any relevant information on the continuous dynamics of the system. From these annotations (in ACSL or Frama-C for instance), proof obligation are extracted, and discharged using Coq [START_REF] Boldo | Coquelicot: A user-friendly library of real analysis for Coq[END_REF] or PVS [START_REF] Herencia-Zapana | PVS linear algebra libraries for verification of control software algorithms in C/ACSL[END_REF].

Our previous work

In the same vein, our work is interested in the definition of generic and reusable models to design and verify hybrid systems. Our approach is based on refinement and proof with the Event-B method, and on a generic model.

Such generic model has been defined [START_REF] Dupont | Proof-based approach to hybrid systems development: Dynamic logic and Event-B[END_REF] and improved [START_REF] Dupont | Event-B hybridation: A proof and refinement-based framework for modelling hybrid systems[END_REF], and has already been used on various case studies, including an automatically braking car [START_REF] Dupont | Proof-based approach to hybrid systems development: Dynamic logic and Event-B[END_REF] and a signalised left-turn assist system [START_REF] Dupont | Hybrid systems and Event-B: A formal approach to signalised left-turn assist[END_REF], as well as in the context of railway systems [START_REF] Stankaitis | Modelling hybrid train speed controller using proof and refinement[END_REF].

In our later work, we took interest in the architectural features of hybrid and cyber-physical systems. In particular, we studied the case of one controller controlling several plants with a case study based on liquid tanks [START_REF] Dupont | Handling refinement of continuous behaviors: A refinement and proof based approach with Event-B[END_REF]. This case study is expanded to build a model featuring several controllers each controlling one plant [START_REF] Dupont | Formally verified architecture patterns of hybrid systems using proof and refinement with Event-B[END_REF] (so-called many-to-many). We use to derive common features and rules for such systems.

In this paper, we put together the case studies formerly developed and expand on them to build proper reusable formal design patterns, under the form of generic models. In particular, we investigate the proof aspect of these patterns, and provide help in discharging them, based on the form of the model, guaranteed by the use of the patterns. Such patterns put together offer the capability to a CPS designer to build any specific system via a series of pattern applications, starting with the generic model. Reusability of models and proofs is central in this approach.

Last, we also propose a discussion on the feasibility of the application of such patterns, as they introduce constraints that influence the possible behaviours of the system.

Component-based design of hybrid systems

Hybrid systems with a high level of complexity are substantially harder to model and verify. A common technique to overcome this problem is to decompose the system in several simpler components, for which verification is easier, or, dually, to use common basic components and to compose them together to build a complex system. Architecture, in terms of how the components of a hybrid system interact, is thus an essential phase of hybrid system design.

When performing composition/decomposition, care must be taken to ensure each component's behaviour is compatible with the behaviour of other components. Additionally, the specific behaviour of each sub-component shall guarantee the safety requirements expressed on the whole system expressed in the form of a global invariant. This design process has been set up by different approaches.

To that extent, the work of Lunel et al. [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] extends the hybrid program modelling approach [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF] with two composition operators, that permit a new system to be built from two existing systems. The authors have also extended the proving system, enabling proof decomposition: any proof on the global system can be decomposed into simpler proofs, under the condition that the operators are correctly used.

More generally, refinement operations are the support of system composition and decomposition steps. It allows to focus on a system at an abstract level and refine to a more complex system with the same properties, effectively balancing the verification effort. This technique is commonly used in approaches such as Event-B and CSP, are thus made available in their hybrid extensions (Hybrid Event-B [START_REF] Banach | Pliant modalities in Hybrid Event-B[END_REF][START_REF] Banach | Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines[END_REF] and Hybrid CSP [START_REF] Jifeng | A classical mind[END_REF]). Hybrid CSP is successfully used in the development of the Chinese lunar lander [START_REF] Zhao | Formal verification of a descent guidance control program of a lunar lander[END_REF] and in the verification of level 3 of the Chinese Train Control System (CTCS-3) [START_REF] Zou | Verifying Chinese train control system under a combined scenario by theorem proving[END_REF].

In the same vein, differential refinement logic [START_REF] Loos | Differential refinement logic[END_REF] also enables differential dynamic logic (dL) to refine a system and decompose it, in order to ease the proving process and improve the re-usability of its components. It introduces the notion of differential invariants to prove the correctness of this refinement. This approach has been applied to model hybrid systems like car control system [START_REF] Quesel | How to model and prove hybrid systems with KeYmaera: a tutorial on safety[END_REF], train control system [START_REF] Platzer | European train control system: A case study in formal verification[END_REF], flight collision avoidance system [START_REF] Platzer | Formal verification of curved flight collision avoidance maneuvers: A case study[END_REF] and mobile robots and surgical robots [START_REF] Kouskoulas | Certifying the safe design of a virtual fixture control algorithm for a surgical robot[END_REF].

Banach extended the Event-B modelling language to Hybrid Event-B [START_REF] Banach | Pliant modalities in Hybrid Event-B[END_REF][START_REF] Banach | Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines[END_REF] by other constructs that enable the modelling of hybrid systems. In particular, it proposes the possibility of defining a whole system based on the modelling of several components, specified and interacting through their interfaces connecting the components with one another. The defined approach provides with a number of assumptions and requirements, under the form of proof obligations, to establish the correctness of the system. The defined model leads to a set of proof obligations that ought to be discharged. Several applications have been reported in [START_REF] Banach | Formal refinement and partitioning of a fuel pump system for small aircraft in Hybrid Event-B[END_REF][START_REF] Banach | Hemodialysis machine in hybrid Event-B[END_REF].

Contribution of this paper

In this paper, our objective is to show how our Event-B based generic model for hybrid systems design can be used to define generic hybrid systems patterns defining different architectures of such systems. We specify three Event-B based models for three architectural patterns addressing different types of control:

• control of a single plant, where one controller handles one plant;

• centralised control of multiple plants, where one controller handles several plants;

• distributed control of multiple plants, where several controllers each handle one plant and satisfy global properties.

All these patterns ensure safety properties through the guarantee of the defined invariants. Throughout this article we will use the same case study, and show how the different architectural patterns are instantiated to obtain a concrete model associated with this case study.

Organisation of this paper

Our paper is structured as follows. Section 2 recalls the basics of the Event-B modelling language. Section 3 presents the mathematical extensions, in the form of formal theories, of the Event-B modelling language to integrate both discrete and continuous modelling in the same setting. It also includes the basic concepts of the hybrid systems generic model we defined. Section 4 describes a case study, which is used throughout this article for modelling different classes of controllers using the three architectural patterns sketched above. The next sections are devoted to the presentation of these architectural patterns. Sections 5, 6 and 7 present the single-to-single, single-to-many and many-to-many architectural patterns respectively. Each pattern description outlines the Event-B formal development, the corresponding proofs and its application to the proposed case study. Finally, Section 8 concludes the paper and outlines some possible future work.

Event-B and its Extension Using Theories

Event-B [START_REF] Biro | Modeling in Event-B: System and Software Engineering[END_REF] is a state-based modelling language primarily established on set theory and first order logic. It enables the correct-by-construction approach to the design of a complex and large system.

A set of events allows for state changes2 (see Table 1). For each model, a set of proof obligations (see Tables 2a and2b) is generated automatically. Event-B is equipped with powerful proof systems, tactics, including a set of proof rules for formal reasoning. The system model consists of an abstract model that leads to the final concrete model, where each refinement introduces additional features and required safety properties that adopt different design decision. Machines (Table 1.b). Machine is another modelling component to describe model behaviour as a transition system using core elementary components such as variables x, invariants I(x), theorems T mch (x), variants V(x) and events evt.

Context Machine Refinement CONTEXT Ctx MACHINE M A MACHINE M C SETS s SEES Ctx REFINES M A CONSTANTS c VARIABLES x A VARIABLES x C AXIOMS A INVARIANTS I A (x A ) INVARIANTS J(x A , x C ) ∧ I C (x C ) THEOREMS T ctx THEOREMS T mch (x A ) ... END VARIANT V(x A ) EVENTS EVENTS EVENT evt C EVENT evt A REFINES evt A ANY α A ANY α C WHERE G A (x A , α A ) WHERE G C (x C , α C ) THEN WITH x A :| BAP A (α A , x A , x A ′ ) x A′ , α A : W(α A , α C , x A , x A′ , x C , x C ′ ) END THEN ... x C :| BAP C (α C , x C , x C ′ ) END ... (a) (b) (c)
Each event is guarded with predicate and is used to update state variables using Before-After Predicates (BAP) relating current (x) and next (x ′ ) values of state variables. It defines a guarded transition.

(1) Theorems Refinements (Table 1.c). Refinement is a process of introducing different characteristics of systems related to functionality, safety and reachability at different abstraction levels. In particular, it decomposes the machine, a state-transition system, into a less abstract one, with more design decisions resolved (refined states and events) moving from an abstract level to a less abstract one (simulation relationship). A set of new gluing invariants J(x A , x C ) relating to abstract and concrete variables always ensures the correctness of the system and the preservation of the property.

A ⇒ T ctx A ∧ I A (x A ) ⇒ T mac (x A ) (2) Invariant A ∧ I A (x A ) ∧ G A (x A , α A ) preservation ∧BAP A (x A , α A , x A ′ ) (INV) ⇒ I A (x A′ ) (3) Event A ∧ I A (x A ) ∧ G A (x A , α A ) feasibility (FIS) ⇒ ∃x A′ • BAP A (x A , α A , x A′ ) (4) Variant A ∧ I A (x A ) ∧ G A (x A , α A ) progress ∧BAP A (x A , α A , x A′ ) ⇒ V(x A′ ) < V(x A ) (a) Machine Proof obligations (5) Event A ∧ I A (x A ) ∧ J(x A , x C ) Simulation ∧G C (x C , α C ) (SIM) ∧W(α A , α C , x A , x A′ , x C , x C′ ) ∧BAP C (x C , α C , x C ′ ) ⇒ BAP A (x A , α A , x A ′ ) (6) Guard A ∧ I A (x A ) ∧ J(x A , x C ) Strengthening ∧W(α A , α C , x A , x A′ , x C , x C′ ) (GS) ∧G C (x C , α C ) ⇒ G A (x A , α A ) (7) Invariant A ∧ I A (x A ) preservation ∧G C (x C , α C ) (INV) ∧W(α A , α C , x A , x A′ , x C , x C′ ) ∧BAP C (x C , α C , x C ′ ) ∧J(x A , x C ) ⇒ J(x A ′ , x C ′ ) (b) Refinement Proof obligations
Proof Obligations (POs) and property verification. Tables 2a and2b show a set of proof obligations for the machine and its refined model. Note that these POs are generated automatically and guarantee Event-B model consistency, including refinements. In order to establish the correctness of the defined model, all the generated POs must be proven.

Rodin. It is an Eclipse based IDE for Event-B project management, model edition, refinement and proof, automatic PO generation, model checking, model animation and code generation. It is equipped with standard provers, including support for external provers such as SMT solvers. A plug-in [START_REF] Butler | Practical theory extension in Event-B[END_REF] is also available to support the development of mathematical theories. More details on the Event-B method and Rodin are available in [START_REF] Biro | Modeling in Event-B: System and Software Engineering[END_REF] and [START_REF] Abrial | Rodin: an open toolset for modelling and reasoning in Event-B[END_REF] respectively.

Extensions with Mathematical Theories

Event-B's expression language is based on first-order logic and set theory, which is mathematically low level. This particularity makes it very expressive, but higher-level constructs are often hard to express and poorly reusable. To address this issue, an extension has been proposed [START_REF] Abrial | Proposals for mathematical extensions for Event-B[END_REF] to define a new type of component, the theories. The syntax for theories is detailed in Listing 1. A theory allows to define type-generic data-types with various constructors (DATATYPE clause), together with operators, either directly or axiomatically defined. Abstract types may also be defined, similarly to carrier sets in contexts. Types and operators defined in a theory can be used seemlessly in models.

Operators are associated to well-definedness (WD) conditions, that are predicates that characterise when the operator is correctly used (e.g. a/b is well-defined if and only if b 0). Upon using an operator with a WD condition in a model, a WD proof obligation is automatically generated.

Last, a theory can define a number of axioms and theorems, and even proof rules (specific rewriting and inference rules), that generally encode properties on the operators and types of the theory. These properties may be referenced during the proving process.

A Generic Event-B Model for Hybrid Systems

Although Event-B is adapted to the modelling of systems in general, it lacks several features to be able to model hybrid systems. Fortunately, Event-B's expression language is based on first-order logic and set theory, which permits to express required continuous features for modelling hybrid behaviour.

In this section, we present a framework for the formal design of hybrid system. This presentation is based on our previous work [START_REF] Dupont | Event-B hybridation: A proof and refinement-based framework for modelling hybrid systems[END_REF][START_REF] Dupont | Correct-by-construction design of hybrid systems based on refinement and proof[END_REF], where we have defined a generic framework for formal hybrid system modelling in Event-B. This generic model defines the core modelling concepts for designing controller-plant loop hybrid systems. It formalises hybrid automata in Event-B, and brings to classical Event-B an implementation of Hybrid Event-B concepts [START_REF] Banach | Core Hybrid Event-B I: Single Hybrid Event-B machines[END_REF].

Note that this section is a summary of these contributions, which are more detailed in the aforementioned publications.

Theories for Event-B Mathematical Extensions for Hybrid Systems Modelling

The nature of hybrid systems requires to handle continuous and discrete features at the same level during modelling and proof. The Event-B extension mechanism enables the definition of such features in a generic and reusable way. In particular, we have defined Event-B theories for handling reals, continuous functions, and differential equations as well as their associated properties. These theories have already been used in the development of several case studies [START_REF] Dupont | Proof-based approach to hybrid systems development: Dynamic logic and Event-B[END_REF][START_REF] Dupont | Hybrid systems and Event-B: A formal approach to signalised left-turn assist[END_REF][START_REF] Dupont | Handling refinement of continuous behaviors: A refinement and proof based approach with Event-B[END_REF]. The complete theories are available at https://irit.fr/~Guillaume.Dupont/models.php.

In the following, we present some of these theories, as our developments heavily rely on them. Figure 2 present the general architecture for the defined theories, and how they are related to each other. Theories are categorised as follow:

• General Algebra: a set of theories that define the basic structures of general algebra: monoids, groups, rings, etc.;

• Reals: two theories that define the real numbers set with its associated operators and properties, as well as intervals;

• Functions: theories that bring additional structure and properties to functions, and in particular continuity and derivability, as well as the overall concept of piecewise defined functions;

• Differential Equations: a theory that defines the concept of differential equations as well as various useful related objects and properties to handle them;

• Approximation: a pair of theories that define the fundamental concepts needed to handle approximations, useful in the case of linearisation for example;

• Domain Theories: various theories for handling specific types of systems: cars, water tanks, robots, etc.

All of the above theories, except approximation, have been set up in the study developed in this paper. Regarding domain theories, we have defined the relevant theories related to the description of the shape of specific liquid tanks.

The next section shows an extract of the theories allowing to model differential equations. Only the relevant concepts necessary to understand this paper are introduced. Modelling hybrid systems requires the introduction of multiple specific features which are defined below.

• DE(S ) type for differential equations for which solutions are valued in set S ;

• ode( f, η 0 , t 0 ) represents the Ordinary Differential Equation (ODE) η(t) = f (η(t), t) with initial condition η(t 0 ) = η 0 (note that we could define other constructors for other types of dynamics);

• solutionOf(D, η, E) is the predicate stating that function η is a solution of equation E on subset D;

• Solvable(D, E, H) is the predicate stating that equation E has a solution defined on subset D so that the solution satisfies the constraint H;

• An encoding of the Cauchy-Lipschitz theorem, that allows to demonstrate the solvability of a given equation under some specific conditions;

These features have been encoded in a theory from which we show a snippet in Listing 2 (the theory accumulates more than 150 operators and 350 properties).

Other, more specialised expressions and predicates are defined (FlowEquation, FlowODE) in additional theories. Note that all these definitions use algebraic datatypes together with axioms, theorems and proof rules.

System State Modelling

Modelling hybrid systems requires the definition of state variables to characterise both discrete and continuous concepts associated with a system. The definition of the continuous state variables is time dependent.

Time.

A notion of time is needed to define continuous behaviour. We thus introduce dense time t ∈ R + , modelled as a continuously evolving variable.

System state. The state of the system is represented by variables. Because of its hybrid nature, we need two types of variables in order to represent its discrete and continuous aspects:

• discrete variables x s ∈ STATES, that represent the controller's state (or mode automaton). They evolve in a point-wise manner, through instantaneous changes.

• continuous variables x p ∈ R + → S , that represent the plant's physical quantities, and evolve continuously. They are modelled as functions of time, valued in S .

State Variables Assignment

Continuous variables are essentially functions of time and are at least defined on [0, t[ (where t is the current time). Updating such variables thus requires to 1) make the time progress from t to t ′ > t, and 2) append to the already existing function a new piece corresponding to its extended behaviour (on [t, t ′ ]) while ensuring its "past" (i.e. whatever happened during [0, t[) remains unchanged.

Similarly to the classic Event-B's before-after predicate (BAP), we define a continuous before-after predicate (CBAP) operator, denoted :| t→t ′ , as follows:

x p :| t→t ′ P(x s , x p , x ′ p ) & H ≡ [0, t[◁x ′ p = [0, t[◁x p (PP) ∧ P(x s , [t, t ′ ] ◁ x p , [t, t ′ ] ◁ x ′ p ) (PR) ∧ ∀t * ∈ [t, t ′ ], x ′ p (t * ) ∈ H (LI)
We use the notation CBAP(x s , x p , x ′ p ) as an abbreviation for PP(x p , x ′ p ) ∧ PR(x s , x p , x ′ p ) ∧ LI(x p , x ′ p ). The operator consists of 3 parts: past preservation and coherence at assignment point (PP), before-after predicate on the added section (PR), and local invariant preservation (LI). The discrete state variables x s do not change in the interval [t, t ′ ] but the predicate P may use them for control purposes.

Note that this operator is well-defined if and only if t ′ > t, as otherwise the interval [t, t ′ ] would not be well-defined.

From the above definition, shortcuts can be introduced for readability purposes:

• Continuous assignment: x := t→t ′ f & H ≡ x :| t→t ′ x ′ = f & H • Continuous evolution along a solvable differential equation E ∈ DE(S ): x :∼ t→t ′ E & H ≡ x :| t→t ′ solutionOf([t, t ′ ], x ′ , E) & H
Note that, similarly to Event-B's BAP assignment operator, the CBAP operator is designed to be fundamentally nondeterministic and with as few constraints as possible, so that it can be used efficiently and conveniently in conjunction with refinement.

Intuitively, non-determinism in the system's behaviour enables to delay some design decisions: we can describe the dynamics of an abstract model using high-level constraints (e.g. "dynamics shall be expressed as the decreasing solutions of a solvable differential equation"), and then provide actual concrete dynamics in a later refinement, making sure they verify these constraints (e.g. "dynamics are given by ẋp = -1").

In practice, this permits the use of event parameters in models (that can be later refined with concrete values using witnesses), and also allows us to use powerful existence theorems, that may not be conclusive with regard to solution uniqueness (e.g. Peano-Lindelöf theorem).

In addition, and contrary to other approaches (e.g. Hybrid Event-B and Hybrid Programs), no assumptions are made about the nature of the dynamics used in the CBAP. This enables the user to propose any kind of behaviours, including rich constructs or even unconventional edge-cases, without having to modify the method in any way, and only by defining/integrating the appropriate theories. However, proof must still be performed, which may be difficult in the case of particularly complex dynamics and depending on the theories defining these dynamics. Many hybrid systems behaviour and structure follow the pattern of Figure 4, called controller-plant loop configuration. In this setting, a hybrid system consists of a discrete controller (Ctrl) controlling a plant (Plant) characterised by continuous behaviour. The controller senses data issued from the plant, and may influence the plant behaviour through of actuators (e.g. motors, pumps, etc.). The controller may also retrieve commands from a user or another controller, and the plant itself is subject to environmental conditions, for instance wind, temperature, etc.

A Generic Event-B Model for Hybrid Systems

Following this pattern, inline with the definitions of Sections 3.1.1 and 3.1.2, we propose a generic Event-B model of hybrid systems. This model is at the core of our work: other development patterns (such as the architectural patterns presented in this paper) are formalised as refinements of this generic model.

VARIABLES t , x s , x p INVARIANTS i n v 1 : t ∈ R + i n v 2 : x s ∈ STATES i n v 3 : x p ∈ R + → S i n v 4 : [0, t] ⊆ dom(x p )
Listing 3: Generic Time, Discrete and Continuous States

Model state. The generic model deals with three variables. x s represents the controller's discrete state (associated to Ctrl in the diagram) that belongs to the STATES set consisting of the states of the system's mode automaton.

x p is the system's continuous state (corresponding to the Plant's state). It is a function of time (inv3) valued in the (continuous) state space S , usually R n . It represents the physical quantities that are sensed and/or controlled. Last, we recall that variable t models the physical, dense time.

Model behaviour. The defined model follows the control-command principle depicted in Figure 4. Two categories of events are defined. Discrete events are instantaneous, in the sense that time does not progress while they are being triggered. They are associated with changes in the state of the mode automaton either internal (Transition event) or induced by the sensing of the plant's state (Sense event). Continuous events, on the contrary, are associated to the passing of time. They describe the Plant's behaviour, either following environmental changes (behave event) or caused by actuation (actuate event). Note that all these generic events will be refined later for developing particular hybrid systems. Sense. Sensing events (corresponding to sense arrow of Figure 4) model changes in the controller induced by the reading of the plant's state, generally obtained from sensors. As they are fired according to the plant's state and to the mode automaton's state, they are guarded by a predicate over x p (t) and x s (grd3 of Sense on Listing 4). The purpose is to change state x s of the mode automaton (action act1).

Discrete Events

Transition ANY s WHERE g r d 1 : s ∈ P1 ( STATES ) THEN a c t 1 : x s :∈ s END Sense ANY s , p WHERE g r d 1 : s ∈ P1(STATES) g r d 2 : p ∈ P(STATES×R × S ) g r d 3 : (x s → t → x p (t)) ∈ p THEN a c t 1 : x s :∈ s END

Continuous Events

Behave ANY eq , t ′ WHERE g r d 1 : eq ∈ DE(S ) g r d 2 : Solvable([t, t ′ ], eq, ⊤) THEN a c t 1 : t, x p :∼ t→t ′ eq & ⊤ END Actuate ANY eq , s , H , t ′ WHERE g r d 1 : eq ∈ DE(S ) g r d 2 : Solvable([t, t ′ ], eq, H) g r d 3 : s ⊆ STATES g r d 4 : x s ∈ s g r d 5 : H ⊆ S g r d 6 : x p (t) ∈ H THEN a c t 1 : t, x p :∼ t→t ′ eq & H END
Listing 5: Generic Behave and Actuation Events Behave. Behave events (corresponding to the environment arrow of Figure 4) represent changes in the plant due to the environment: rain, wind, etc. They are encoded as shown on the left-hand side of Listing 5.

These events enforce, in action act1, the dynamics of the plant to comply with a differential equation under solvability condition (gdr2) but without any condition on the state of the mode automaton.

Actuate. Actuation events (corresponding to the actuate arrow of Figure 4) model changes in the plant induced by the controller (generally performed by actuators). They are encoded as on the right-hand side of Listing 5.

These events enforce, in action act1, the dynamics of the plant to comply with a differential equation under solvability condition (gdr2) and a constraint H on the plant evolution domain (gdr5 and gdr6). Moreover, unlike for Behave, since Actuate results from a change in the controller, it is guarded by a predicate on the mode automaton (gdr4).

As mentioned above, both Behave and Actuate are continuous events. They rely on the continuous evolution operators defined in Section 3.1.3. Both events enforce plant behaviour by setting up a corresponding differential equation. Because these events are based on the CBAP operator :| t→t ′ (and its derivatives), they are associated to a feasibility proof obligation, that ensures there exists (t ′ , x ′ p ) such that x p :| t→t ′ P(x s , x p , x ′ p ) & H holds. Establishing feasibility of a particular predicate in a refinement is completely tied to the nature of the predicate. When using differential equations, solvability needs to be asserted (by virtue of guard gdr2) using specific theorems such as the Cauchy-Lipschitz theorem, or any other property associated to the considered differential equation.

Semantics

The semantics of hybrid models we use is close to the one of Hybrid Event-B [START_REF] Banach | Core Hybrid Event-B I: Single Hybrid Event-B machines[END_REF], hybrid programs in [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF] or continuous action systems [START_REF] Back | Generalizing action systems to hybrid systems[END_REF][START_REF] Meinicke | Continuous action system refinement[END_REF].

In classical Event-B semantics, each model is associated with a discrete state-transition system, in which transitions are the fired machine events and states consist of the machine's variables. A system is hence characterised by a set of admissible traces i.e. a set of fired events that abide by the system's invariants.

In our approach, discrete events are timeless, while continuous ones are associated to the passing of time. In order to properly handle the modelling of continuous behaviour, the semantics of Event-B is enhanced to handle modelling of continuous phenomena which are, in nature, different from discrete behaviour. We have identified two categories of events: discrete (instantaneous) events, which use discrete assignment operators such as :| and := and continuous (not instantaneous) events that span over some duration and use continuous assignment operators, namely :| t→t ′ and := t→t ′ . Note that, if several (continuous or discrete) event guards are enabled, these enabled events are fired non-deterministically.

A model is then defined as follows. After initialisation, continuous events (Behave and Actuate events) execute continuously unless a discrete, instantaneous event is enabled (either a Sense or a Transition event). In this case, discrete events are preemptive, meaning they are executed before the control is handed over to continuous events. This protocol ensures that when the conditions (events' guards) are met, the controller is able to trigger control actions (Sense or Transition) that may or may not change the continuous behaviour of the plant (through triggering an Actuate event). Unlike Actuate, the Behave event neither requires a control action to be triggered nor any plant evolution constraint H. Sensing actions using the Sense event will re-establish the correct plant behaviour via the control loop in order to further trigger an Actuate event.

Note that the proposed semantics is the one proposed by R. Banach for Hybrid Event-B [START_REF] Banach | Core Hybrid Event-B I: Single Hybrid Event-B machines[END_REF][START_REF] Banach | Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines[END_REF], where discrete events correspond to mode events, while continuous events correspond to pliant events.

In our approach, we have formalised the features of Hybrid Event-B within Event-B, in order to offer an operational framework relying on the Rodin platform -which is missing for Hybrid Event-B. Proceeding in this way, we can use Rodin to model hybrid systems with both discrete and continuous behaviours, including support for model development and proofs.

Time-triggered vs. event-triggered. The semantics we proposed is so-called event-triggered: discrete phenomena are considered timeless events, that may occur at any time and interrupt continuous phenomena. This kind of semantics is relatively abstract and simplifies a number of problems, and in particular zero-crossing.

Formally, zero-crossing is when a controller "misses" events, i.e. when the continuous variable crosses a domain (guard, evolution domain) without the controller detecting it. With event-triggered semantics, we can always assume that the controller notices the continuous variable crossing the domain at the exact time point it does so.

Comparatively, time-triggered semantics is less abstract: it requires that the controller is always able to detect variable crossing at the very latest when it occurs (and ideally before). Time-triggered semantics is harder to prove but easier to implement. In practice, one may derive a concrete time-triggered model from an abstract event-triggered one (with a refinement step, for instance), as to benefit from the easier proof with event-triggered semantics while approaching a level of abstraction closer to implementation.

Zeno behaviour. The duration of continuous events may be arbitrarily small, and even infinitely small, so that two discrete events are infinitely close. This may lead to a situation known as Zeno paradox, where an infinite number of discrete events is triggered in a finite amount of time.

The Generic Model in Rodin

The generic model is the entry point for the method. Specific hybrid system models are obtained by refining it, providing the various witnesses issued from event parameters and substituted variables. In itself, this model generates 13 proof obligations that are easily discharged. Among them there is an important obligation stating that if equation e is solvable then x :∼ t→t ′ e is feasible.

This approach has been successfully applied to various case studies. [START_REF] Dupont | Proof-based approach to hybrid systems development: Dynamic logic and Event-B[END_REF][START_REF] Dupont | Hybrid systems and Event-B: A formal approach to signalised left-turn assist[END_REF] show a class of systems with one controller and one plant while [START_REF] Dupont | Handling refinement of continuous behaviors: A refinement and proof based approach with Event-B[END_REF] demonstrates the possible use of the method for a system with one controller and several plants.

Models for the generic approach, including the above-mentioned case studies can be found at https://www.irit. fr/~Guillaume.Dupont/models.php.

A Case Study

To demonstrate how the various architectural patterns we propose are applied to model specific hybrid systems, we have chosen a case study that is classically exemplified in control theory literature. The objective of the case study is to control the volume of liquid in one or more tanks. In particular, the defined control must keep the volume level between given minimum and maximum levels. We identified the following cases based on the defined patterns.

• Mono control system where one tank is controlled by a unique controller;

• Centralised control where multiple tanks are controlled by a single controller;

• Distributed control where a set of communicating controllers, each of which controls one tank, that contribute to the control of the cumulative volumes of each tank.

In the next two sections, we first describe the case study and highlight two safety requirements. Then, a domain theory axiomatising the general characteristics and properties of tanks is presented. This theory provides relevant properties used in further developments.

Description of the Case Study

Figure 7 depicts an abstract representation of the case study we use throughout this paper. The system consists of tank(s) containing a volume of liquid, of arbitrary shape and architecture (abstracted). It is connected to a generic controller, that is able to actuate pumps (an input and an output pump) to fill or empty the tank(s). The connected controller can also sense the volume in the tank(s).

The goal of the system is to maintain the volume of liquid inside the tank(s) between too given constants V low and V high (SAF1), and also to ensure that the flow in the tank is bounded by a constant ∆V max , in order to avoid turmoil (SAF2). Formally

∀t, V low ≤ V(t) ≤ V high ∧ | V(t)| ≤ ∆V max
Last, we suppose that activating the input pump will fill up the tank(s), and activating the output pump will empty it. Also, when no pump is active, the volume in the tank does not vary. Apart from that, there is no additional hypothesis on the system at this level of description.

A Theory of Water Tanks

Water tanks are associated with a number of specific phenomena and properties: pumps physical modelling, specific differential equations, etc. These features have been formalised in a domain specific theory of water tanks.

The theory is split in two parts: a theory for valves and a theory for flows. Extracts for both these theories are given in Listing 6. They define a number of operators used in the model when instantiating the patterns, as well as several theorems and axioms, used during the proving process. Valves. The theory first defines the Status datatype as an enumeration specifying whether a valve is open (ValveOpen) or closed (ValveClosed). Secondly, the theory defines the InOutValve product type, which includes the status of two valves (an input and an output one). This type is associated with a single constructor, InOut, which allows both statuses to be set.

t i o n ∀η • η ∈ R → R ∧ D ⊆ dom(η) ∧ solutionOf(D, η, e) ⇒ isFlow(s, D, η, Q min , Q max ) . . .
These types are associated with convenient valve opening and closing operators (closeIn, openOut, etc.). The theory also provides a way to associate a real number with the status of the valve, ValveClosed being associated with 0 and ValveOpen with 1. Finally, the theory defines the set of possible valve combination, InOutPossible.

Flow. This second theory is based on the previous one and on the differential equation theory. It defines several operators to characterise the various features of any tank. In particular, it proposes an enumeration datatype for the possible tank states TankState (see Section 5.2.1). It also makes accessible various operators to handle the generic concept of flow.

The predicate isFlow is defined, that is true for a domain D ⊆ R, a state s ∈ TankState, a function Φ ∈ R → R with D ⊆ dom(Φ) and two bounds Q min and Q max (in R) if and only if Φ behaves according to s on D, and is bounded by Q min and Q max .

In this context, behaving according to s typically means that Φ is decreasing on D if state s is Emptying, constant if state is Stable and so on.

This predicate is adapted to be used on differential equation (isFlowEq), to check that the solutions of given equation are adequate with regard to the given state. This operator is further specialised to ODE, since the ODE's function's sign gives the monotonicity of the solution. Additionally, the theory gives a simple ODE for modelling the flow of a tank (FlowODE, corresponding to the one presented in Section 6.3). It also proposes an ODE for a tank with no flow, used for initialisation. In addition, the TankModeChange predicate is defined for the particular case of two tanks. It links a global state (state) representing a global view of the two tanks to the local states of each tank (io 1 and io 2 ). It is studied more thoroughly in Section 6.3.1.

Finally, we define various theorems aimed at handling the defined operators, especially the ODEs and their solvability.

The following sections address this case study, under different hypotheses, and most importantly using different architectures, to illustrate the formalised architectural patterns we propose in this paper.

Single-to-Single Architectural Pattern

The single to single architectural pattern is the basic one. It represents the case of one controller for one plant. This pattern represents the basic pattern from which all the others are derived by refinement.

The S2S pattern

The single-to-single (S2S for short) architectural pattern is depicted in Figure 9. It is the general structure of hybrid systems handled by the generic model, and consists of a single controller, controlling a single plant.

This pattern corresponds to refining and instantiating the generic model for a given hybrid system. It is not described in this section, as it has been detailed in Section 3. Next section shows how it is instantiated to model the case study of a single controller for a single tank.

Application to Case Study -Abstract Tank Model

The first step for addressing this case study is to model the abstraction of the system depicted in Figure 7. Formally, the abstract tank model is a refinement of the generic model.

Preliminary Study

Plant description. The controlled plant is an abstract tank containing a volume V(t) ≥ 0 of liquid. This tank is finite and can contain a maximum volume of V max > 0. The plant is tied to two pumps, one input pump able to fill-up the tank (i.e. increase V(t)) and another to empty it (i.e. decrease V(t)). Note that the behaviour of V(t) is unspecified when both pumps are operating at the same time.

At this point, no hypothesis is made on the shape of the tank, and no hypothesis is made on the exact behaviour of the pumps, except that 1) when the input pump is open the volume increases, 2) when the output pump is open the volume decreases, and finally 3) when no pump is open the volume does not change.

Consequently, for this model, the differential equation describing the volume's behaviour is unknown, although it is constrained by the hypotheses on the pumps' behaviour.

Note that, for convenience, it is assumed that tank initially contains some arbitrary initial volume V 0 , such that

V low ≤ V 0 ≤ V high .
Controller description. The controller's task is to actuate the input and output pumps, in order to fill or empty the tank. Concretely, it operates in 4 modes, and switches from one to another when needed, to preserve safety. These modes are:

• stable, the volume does not change (i.e. V is a constant function). Provided V remains within the bounds, the controller can always switch to this mode;

• emptying, the volume is decreasing. The controller may switch to this mode if V > V low , and it switches automatically to it when V = V high ;

• filling, the volume is increasing. The controller may switch to this mode if V < V high , and it switches automatically to it when V = V low ;

• normal, the volume varies arbitrarily. The controller may switch to this mode if V is within the bounds. It is a default mode, where liquid is flowing freely.

These modes induce 4 transition events, allowing to visit each state, and 2 sensing events, that detect when the volume reaches a bound and puts the system in the corresponding correcting mode. Note that, when actuating the pump, the controller must make sure that the volume level does not change too rapidly, i.e. its derivative is bounded ( V ≤ ∆V max ).

Requirements. In summary, the system requirements are described as follows:

FUN1 the volume varies in the tank, it is decreasing in emptying mode, increasing in filling mode, constant in stable mode, and safely varying in normal mode; ENV1 the volume is physically bounded by 0 and some constant

V max : ∀t ∈ R + , 0 ≤ V(t) ∧ V(t) ≤ V max ;
SAF1 the volume must always remain within the set bounds, V low and V high :

∀t ∈ R + , V low ≤ V(t) ∧ V(t) ≤ V high ;
SAF2 the variation of the volume ( V(t)) is always below the maximum allowed variation

∆V max : ∀t ∈ R + , | V(t)| ≤ ∆V max .

Event-B Development

The preliminary study for this system leads to the definition of an Event-B model. This first model (the abstract tank) is based on the generic model presented in Section 3.

CONTEXT A b s t r a c t T a n k C t x EXTENDS G e n e r i c C t x CONSTANTS V max , V low , V high , ∆V max , V 0 AXIOMS axm1 : S = R axm2 : partition(STATES, {Stable}, {Emptying}, {Filling}, {Normal}) axm3-6 : V max , V low , V high , ∆V max ∈ R axm7 : 0 ≤ V low ≤ V high ≤ V max axm8 : ∆V max > 0 axm9-11 : V 0 ∈ R ∧ V low ≤ V 0 ∧ V 0 ≤ V high END Listing 7: Abstract Tank -Context
Constants and axioms. The system requires a number of properties to be written (in addition to the theories of valves and flows presented in Section 4.2), that are identified in an Event-B context, given in Listing 7. This context defines the required constants with associated properties (axm3-11). We also define the system's state-space (R in axm1) as well as the controller modes (axm2), based on those defined in the tank theories (flow and valves).

Machine header. Listing 8 presents the machine's header and initialisation event. The header defines the variables of the system (mainly the continuous state V) with associated properties (inv1-2). inv3 is the gluing invariant of the system (a substitution) while inv4 encodes the environment property ENV1 of the requirements section. Finally, inv5 and inv6 model the safety requirement SAF1 and SAF2 respecitvely.

The system's initialisation is straightforward. The controller starts in stable mode, and the volume is set to the constant V 0 , initial volume contained in the tank.

MACHINE A b s t r a c t T a n k REFINES G e n e r i c SEES

A b s t r a c t T a n k C t x VARIABLES t , x s , V INVARIANTS i n v 1 : V ∈ R → S i n v 2 : [0, t] ⊆ dom(V) i n v 3 : V = x p i n v 4 : ∀t * • t * ∈ [0, t] ⇒ 0 ≤ V(t) ∧ V(t) ≤ V max i n v 5 : ∀t * • t * ∈ [0, t] ⇒ V low ≤ V(t * ) ∧ V(t * ) ≤ V high i n v 6 : ∀t * • t * ∈ [0, t] ⇒ | V(t * )| ≤ ∆V max INITIALISATION WITH x ′ p : V ′ = x ′ p THEN a c t 1 : t := 0 a c t 2 : x s := Stable a c t 3 : V := {0 → V 0 } END Listing 8: Abstract Tank -Machine Header ctrl_transition_normal REFINES Transition WHERE g r d 1 : V(t) < V high g r d 2 : V low < V(t) WITH s : s = {Normal} THEN a c t 1 : x s := Normal END ctrl_sense_too_high REFINES Sense WHERE g r d 1 : V high ≤ V(t) WITH s : s = {Emptying} p : p = STATES × R × {V * | V hight ≤ V * } THEN a c t 1 :
x s := Emptying END Listing 9: Abstract Tank -Transition and Sensing Discrete events. Listing 9 gives a transition and sensing events from the system. ctrl_transition_normal is a transition event that allows the controller to move to normal mode. It is guarded by a condition to preserve safety in this mode.

The sensing event ctrl_sensing_too_high detects when the volume reaches V high (see grd1), and causes the controller to move to emptying mode.

For both events, witnesses (for instantiation) are provided for s and p, reflecting their guards and target state.

Continuous events. Listing 10 presents the actuation of the system. It refines the abstract Actuate event and constrains it in order to ensure the system's invariant holds.

EVENT ctrl_actuate_pumps REFINES Actuate ANY eq , s , t ′ WHERE g r d 0 :

t ′ ∈ R ∧ t < t ′ g r d 1 : eq ∈ DE(S ) g r d 2 : Solvable([t, t ′ ], eq, {V * | V low ≤ V * ∧ V * ≤ V high } g r d 3 : isFlowEq(s, [t, t ′ ], eq, 0, V max ) g r d 4 : s ∈ STATES g r d 5 : x s = s g r d 6 : V low ≤ V(t) ∧ V(t) ≤ V high WITH x ′ p : x ′ p = V ′ H : H = {V * | V low ≤ V * ∧ V * ≤ V high } THEN a c t 1 : V :∼ t→t ′ eq & {V * | V low ≤ V * ∧ V * ≤ V high } END Listing 10: Abstract Tank -Actuation Event
For instantiation purposes, in the WITH clause, x p is substituted with V using the gluing invariant, and a concrete evolution domain H is given to enforce the volume V to remain within the given bounds V low and V high . At this level, the differential equation is still unknown, but it is constrained by the required behaviour of the pumps. These constraints are encapsulated in the isFlowEq predicate (see Section 4.2). Therefore, according to the shape of the concrete tank, any differential equation, modelling the liquid behaviour of this concrete tank, that fulfils the conditions expressed by guards grd2 and grd3 may be used as a witness for the parameter eq at instantiation.

Proofs

At this point, proofs are straightforward. The model generated 64 proof obligations, most of them (around 30%) coming from well-definedness. Simulation and guard strengthening POs (44%) are discharged by exploiting the fact that the events are built by substituting variables/parameters.

Last, invariant proofs (23%), putting apart trivial type-related invariants, rely on the specific constraints given to the model (values for H and use of the isFlowEq predicate), together with the properties these constraints entail, that are given in the tank theories. The remaining POs are related to feasibility (3%).

The single-to-single model serves as a base for the application of the single-to-many and many-to-many patterns, as both plant (single-to-many) and controller (many-to-many) are refined. The single-to-many (S2M for short) pattern appears in scenarios such as the one shown in Figure 14. It represents centralised control systems: multiple plants are controlled by a single controller. It is able to access each plant's state, and influence each plant using separate actuators. In this setup, the difficulty is to enforce a global property on the system, while having separate plants, each with its own properties.

Single-to-Many Architectural Pattern

As a simple example of this kind of situation, one can imagine a set of tanks in which the valves are controlled by a single system. The goal is to maintain, as invariant, a certain volume of liquid between low and high volume levels as a whole (i.e. globally for all the tanks) by opening the output and the input valves as needed. The difficulty of controlling this system comes from the ability to change the volume of multiple tanks while enforcing this invariant (for example, we could have several completely empty tanks while still retaining the property).

Pattern Model

This pattern is presented as a refinement, showing an abstract generic model (denoted as a superscript A) and a refinement (denoted as a superscript C) side by side.

As a matter of simplification, it is assumed that the concrete machine handles 2 continuous state variables (i.e. two plants), but it can easily be extended to use as many continuous state variables as necessary. We also consider that the discrete state does not change from one machine to the other.

Machine Headers

Listing 11 gives the header of the two machines. Following the generic model presented in Section 3, the machines first define a variable for time (t) and a variable for the discrete state (x s ) with associated invariants. Machine The initialisation events for both machines are shown in Listing 12. Here, x A p is substituted using the gluing invariant inv5 and "disappears" thanks to refinement. It is substituted by the new continuous state x C p,1 , x C p,2 . In addition, it is subsequently substituted in the actions by these new variables, and based on the gluing invariant, a witness is provided for x A′ p . This witness allows to maintain the invariant.

M A MACHINE M A VARIABLES t , x s , x A p INVARIANTS i n v 1 : t ∈ R + i n v 2 : x s ∈ STATES i n v 3 : x A p ∈ R → S A i n v 4 : [0, t] ⊆ dom(x A p ) MACHINE M C REFINES M A VARIABLES t , x s , x C p,1 , x C p,2 INVARIANTS i n v 3 1 : x C p,1 ∈ R → S C 1 i n v 3 2 : x C p,2 ∈ R → S C 2 i n v 4 1 : [0, t] ⊆ dom(x C p,1 ) i n v 4 2 : [0, t] ⊆ dom(x C p,2 ) i n v 5 : x A p = f (x C p,1 , x C p,

Discrete Events

It is assumed that the discrete behaviour of the system does not change from the abstract machine to the concrete one (i.e. the controller remains single). This means that transition events remain unchanged. Sensing events, on the other hand, need to be addressed as they have access to a continuous state.

Sense A ANY s , p A WHERE g r d 1 : s ∈ P1(STATES) g r d 2 : p A ∈ P(STATES × R × S A ) g r d 3 : (x s → t → x A p (t)) ∈ p A THEN a c t 1 : x s :∈ s END Sense C REFINES Sense A ANY s , p A WHERE g r d 1 : s ∈ P1(STATES) g r d 2 : p A ∈ P(STATES × R × S A ) g r d 3 : (x s → t → f (x C p,1 (t), x C p,2 (t))) ∈ p A THEN a c t 1 :
x s :∈ s END Listing 13: S2M Pattern -Sensing Event Listing 13 presents the sensing events for the S2M pattern. Note that the event is unchanged, except for the abstract state x A p that is substituted with the concrete state (x C p,1 , x C p,2 ) by exploiting the particular shape of the gluing invariant.

This replacement is sound (see Section 6.2.2) and the resulting guard is equivalent to the guard of the abstract sensing event. Note that, as for any event refinement, it is possible to propose a stronger guard provided that this event remains feasible.

Continuous Events

As the refinement of the S2M pattern affects the system's continuous state, continuous events provide important updates. In this section, we only address the case of the actuation event, since behave can be seen as a simpler (i.e. less constrained) version of the actuation event.

Actuate A ANY P A , s , H A , t ′ WHERE g r d 0 : t ′ > t g r d 1 : P A ∈ (R + → S A ) × (R + → S A ) g r d 2 : Feasible(x A p , [t, t ′ ], P A , H A ) g r d 3 : s ⊆ STATES g r d 4 : x s ∈ s g r d 5 : H A ⊆ S A g r d 6 : x A p (t) ∈ H A THEN a c t 1 : x A p :| t→t ′ P A (x A p , x A′ p ) & H A END Actuate C REFINES Actuate A ANY C , s , H A , t ′ WHERE g r d 0 : t ′ > t g r d 1 : P C ∈ (R + → (S C 1 × S C 2 )) × (R + → (S C 1 × S C 2 )) g r d 2 : Feasible(x C p,1 ⊗ x C p,2 , [t, t ′ ], P C , f -1 [H A ]) g r d 3 : s ⊆ STATES g r d 4 : x s ∈ s g r d 5 : H A ⊆ S A g r d 6 : f (x C p,1 , x C p,2 ) ∈ H A WITH x A′ p : x A′ p = f (x C′ p,1 , x C′ p,2 ) THEN a c t 1 : x C p,1 , x C p,2 :| t→t ′ P C (x C p,1 ⊗ x C p,2 , x C′ p,1 ⊗ x C′ p,2 ) & f (x C p,1 , x C p,2 ) ∈ H A END Listing 14: S2M Pattern -Actuation Event
Listing 14 shows the Actuate event of the S2M pattern. Notice the use of the direct product (⊗) to bind together two functions, in order to be able to use the theory's operators on them.

The only parameter to be changed is P A , replaced by P C . In theory, we would have to provide a witness, but since this is a pattern, it is expected that, at this point, these predicates would actually contain definite values, and a witness would depend heavily on those values.

Local invariant H A is unchanged; instead, guards grd2 and grd6 are updated to use the concrete continuous state (x C p,1 , x C p,2 ) instead of the abstract one, again exploiting the gluing invariant. The evolution domain of the CBAP operator (right-hand side of the &) is modified in a similar way. It is used for establishing simulation (see Section 6.2.3). Note that, equivalently, predicate of the form f (x C p,1 , x C p,2 ) ∈ H A may be replaced by: (

x C p,1 , x C p,2 ) ∈ f -1 [H A ].
Finally, a witness is provided for x A′ p , recalling the gluing invariant.

Proofs

The single-to-many architectural pattern yields multiple proof obligations that need to be proved. Since it is a pattern, these proof obligations are general, and discharging them often requires relying on the particular shape and properties of the model parameters (predicates, variables, and so on).

In this section, we study the generated POs associated with the pattern, and give general techniques to discharge them.

Invariant Preservation

Gluing invariant preservation (PO 7 of Table 2b) shows the correctness of the relation between the abstract and the concrete variables of the system. In the case of the single-to-many refinement, the preservation of the gluing invariant (inv5 of Listing 11) is ensured by the use of witnesses for x A′ p , in particular in continuous events. The preservation of the other invariants (PO 2 of Table 2a), specific to the machine, is to be proven on case-by-case basis. It highly depends on the nature of the invariant and of the system's behaviour.

Guard Strengthening

Guard strengthening (see PO 6 in Table 2b) is a proof obligation that is directly related to refinement, and thus is generated when instantiating the pattern. In our case, we address guard strengthening of guards that involve a continuous state, i.e. the guards of sensing events and the evolution domain consistency of actuation events.

For instance, guard strengthening for sensing events yields the following PO:

A ∧ I ∧ W ∧ x A p = [0,t] f (x C p,1 , x C p,2 ) ∧ (x s → t → f (x C p,1 (t), x C p,2 (t))) ∈ p A ⇒ (x s → t → x A p (t)) ∈ p A
Discharging this PO is straightforward, using the gluing invariant to substitute x A p with f (x C p,1 , x C p,2 ) on the right-hand side of the implication (by noticing that t ∈ [0, t]).

Similarly, we consider the PO associated to evolution domain consistency (grd6 of actuation events):

A ∧ I ∧ W ∧ x A p = [0,t] f (x C p,1 , x C p,2 ) ∧ f (x C p,1 (t), x C p,2 (t)) ∈ H A ⇒ x A p (t) ∈ H A
Using the same technique as for guard strengthening POs in sensing events (i.e. substitution using the gluing invariant) allows to discharge the PO.

Note that the concrete and abstract guards are equivalent. It is always possible to propose a stronger guard in the refinement, provided it implies the abstract one (e.g.

f (x C p,1 (t), x C p,2 (t)) ∈ H ⊆ H A ).

Simulation

Simulation (see PO 5 in Table 2b) is a crucial proof obligation associated with refinement. It ensures that the behaviour of a concrete event simulates the one of the abstract event.

This PO is written as:

A ∧ I ∧ G∧x A′ p = [0,t ′ ] f (x C′ p,1 , x C′ p,2 ) ∧ CBAP(t, t ′ , x C p,1 ⊗ x C p,2 , x C′ p,1 ⊗ x C′ p,2 , P C , f -1 [H A ]) ⇒ CBAP(t, t ′ , x A p , x A′ p , P A , H A )
We can unfold the definition of CBAP (as given in Section 3.1.3) on each side of the implication:

A ∧ I∧G ∧ x A′ p = [0,t ′ ] f (x C′ p,1 , x C′ p,2 ) ∧ [0, t[◁(x C′ p,1 ⊗ x C′ p,2 ) = [0, t[◁(x C p,1 ⊗ x C p,2 ) ⇒ [0, t[◁x A′ p = [0, t[◁x A p (PP) ∧ P C ([0, t] ◁ (x C p,1 ⊗ x C p,2 ), [t, t ′ ] ◁ (x C′ p,1 ⊗ x C′ p,2 )) ∧ P A ([0, t] ◁ x A p , [t, t ′ ] ◁ x A′ p ) (PR) ∧ (x C′ p,1 ⊗ x C′ p,2 ) ∈ [t,t ′ ] f -1 [H A ] ∧ x A′ p ∈ [t,t ′ ] H A (LI)
Using the gluing invariant and the witness (

x A′ p = [0,t ′ ] f (x C′ p,1 , x C′ p,2
)) to substitute x A p and x A′ p in the formula, and by exploiting the properties of the domain restriction operator (◁), the proof for PP and LI are completed.

At this step, the continuous predicate simulation (CPSIM) part of the proof is left to prove:

A ∧ I ∧ G∧ x A′ p = [0,t ′ ] f (x C′ p,1 , x C′ p,2 ) ∧ CBAP(t, t ′ , x C p,1 ⊗ x C p,2 , x C′ p,1 ⊗ x C′ p,2 , P C , f -1 [H A ]) ⇒ P A ([0, t] ◁ x A p , [t, t ′ ] ◁ x A′ p ) (CPSIM)
Such proof is to be conducted on a case-by-case basis, as it highly depends on the form of the predicates P A and P C . Evolution domain f -1 [H A ] can be strengthened in order to give additional properties, used as hypotheses for this proof.

In the case where the event uses the :∼ t→t ′ operator, the proof consists in establishing that the solutions of the concrete equations, once processed through the gluing relation f , yield a function that is a potential solution of the abstract differential equation.

Application to the Case Study

We propose a refinement of the abstract tank model developed in Section 5.2 into a system that consists of one controller controlling two separate tanks of definite shape (see Figure 19), using the single-to-many architectural pattern. The goal of the system remains the same, but the abstract tank is replaced by two cylindrical tanks of known bases and heights. The sensing is also updated to better reflect "real world" situations: only the height is accessible (e.g. thanks to a float), and the controller needs to derive the actual volume based on this height and the parameters of the tank.

Last, the pumps' behaviour is fixed, either fully open or fully closed, and delivers a fixed flow. Note that the volume V i (t) of tank i is given by the formula V i (t) = B i × h i (t). The global volume of the system V(t) is then equal to:

V(t) = B 1 × h 1 (t) + B 2 × h 2 (t) (1)
This expression serves as gluing invariant for the system. Note that it is of the form

x A p = f (x C p,1 , x C p,2 ), with x A p = V, x C p,i = h i and f (h 1 , h 2 ) = B 1 × h 1 + B 2 × h 2 .
The defined pump behaviour is modelled by a differential equation for the h i , based on their status. Let In i and Out i the status of the input and of the output pump respectively (with In i = 1 if the pump is open and 0 otherwise); the variation of liquid height in the tank is expressed as:

∆ i = In i × δ in i -Out i × δ out i (2)
Concretely, the variation of the liquid height is equal to liquid input minus liquid output from the tank. Using this expression, we derive the tanks' ODE:

Φ i (t, h) = ∆ i = In i × δ in i -Out i × δ out i
Note that, in terms of pattern application, we have

S A = S C 1 = S C 2 = R.
Controller description. Apart from the fact that volume is not directly accessible, the controller for this system remains the same as for the abstract one. It operates in the same modes, which are triggered in the same way, replacing V by B 1 h 1 + B 2 h 2 , following the system's gluing invariant. Additionally, as the behaviour of the pumps is known, we define a set of rules that associate the modes of the controller to the state of the pumps: This behaviour is captured and formalised by the TankModeChange predicate, defined in the Flow theory (see Listing 6):

TankModeChange(x s , (In 1 , Out 1 ), (In 2 , Out 2 )) ⇔ (x s = emptying ⇒ In 1 = 0 ∧ Out 1 = 1 ∧ In 2 = 0 ∧ Out 2 = 1) ∧ (x s = filling ⇒ In 1 = 1 ∧ Out 1 = 0 ∧ In 2 = 1 ∧ Out 2 = 0) ∧ . . . (3)
This particular predicate, together with the concrete ODE for the tank allows to enforce requirement FUN1 of the abstract tank, encoded in guard grd3 of event ctrl_actuate_pumps of the AbstractTank model (Listing 10). Concretely, in emptying mode, the differential equation yields decreasing solutions, in filling mode, the differential equation yields increasing solutions, etc.

Note that it is perfectly possible to define other richer behaviours; the difficulty is then to enforce requirement FUN1, or in other words to establish guard strengthening, that preserves safe system behaviour, of grd3 of the abstract event ctrl_actuate_pumps.

Requirements. The requirements of the abstract tank are refined and constrained. In particular, the following items are added:

FUN2 The plant consists of 2 tanks with independent pumps that operate with a constant flow; FUN3 The controller can only sense the height of liquid in each tank; it computes the volume using the sensed height and the parameters of the tanks; ENV2 Both tanks have a given bases B 1 and B 2 , and a given maximum height H 1,max and H 2,max ; the maximal global volume is then Vmax

= B 1 H 1,max + B 2 H 2,max .
Refinement feasibility. The added requirement ENV2 implies that the concrete tanks may not have the same total maximum volume as the abstract tank. This means in particular that there may exist some combination of tanks that violate requirements SAF1 of the abstract tank.

To avoid this situation and enforce correct refinement, it is required that the total maximum volume of the tanks Vmax is greater than the lower bound for the volume V low : Vmax ≥ V low . Without this constraint, the system can never enforce invariant SAF1 at all.

Similarly, the gluing invariant allows to deduce V(t) = B 1 ḣ1 (t) + B 2 ḣ2 (t), and the ODE for the tanks gives the following expression for V:

V(t) = B 1 ∆ 1 + B 2 ∆ 2 .
By rewriting this expression, we observe that:

| V(t)| ≤ B 1 • max(δ in 1 , δ out 1 ) + B 2 • max(δ in 2 , δ out 2 ). It follows that SAF2 is equivalent to the condition B 1 • max(δ in 1 , δ out 1 ) + B 2 • max(δ in 2 , δ out 2 )
≤ ∆V max where every symbol is constant. Note that refinement works by strengthening constraints, meaning that we can establish a correct refinement relationship between the abstract and the concrete tanks where the concrete maximum volume is lower than the higher bound (i.e. V low ≤ Vmax < V high ). In this peculiar situation, half of the invariant is statically enforced (∀t, V(t) ≤ V high ), but the system looses some capabilities: there exist potential values of the abstract state that can never be reached by the concrete state.

This issue is tied to the meaning we give to the abstract model. On the one hand, it may be seen as a bound for the system, i.e. a minimal safety requirement, in which case constraining it is acceptable. On the other hand, it may also be seen as a correctness requirement, meaning that the system must not only comply with the given safety bounds but also ensure the given bounds can be reached. In this case, additional invariant properties related to the reachability of all abstract states must be added to the model.

Event-B Development

Context and axioms. Listing 15 gives the context for the designed system. It encompasses the various constants presented during the preliminary study and their associated properties. In particular, axm13 and axm23 encode the properties discussed in the requirement section of the preliminary study, regarding the feasibility of this refinement.

Moreover, axm14 links the initial value for V (V 0 ) to the initial values of h 1 and h 2 . This is so that we can establish simulation for the initialisation in the machine.

Note that additional useful parameters are found in the tank theories (see Section 4.2). Machine header. The machine's header and initialisation are shown in Listing 16. The machine is, as expected, a refinement of the abstract tank model. Variable V is substituted with variables h 1 and h 2 , and the three are linked via the gluing invariant inv5, directly taken from Equation 1.

CONTEXT 1 C t r l _ 2 T a n k s _ C t x EXTENDS A b s t r a c t T a n k C t x CONSTANTS B 1 , B 2 , H 1,max , H 2,max , h 0 1 , h 0 2 , δ in 1 , δ out 1 , δ in 2 , δ out 2 AXIOMS axm1-4 : B 1 , B 2 ∈ R , 0 < B 1 , 0 < B 2 axm5-8 : H 1,max , H 2,max , h 0 1 , h 0 2 ∈ R axm9-10 : 0 < H 1,max , 0 < H 2,max axm11-12 : 0 < h 0 1 < H 1,max , 0 < h 0 2 < H 2,max axm13 : V high ≤ B 1 H 1,max + B 2 H 2,max axm14 : V 0 = B 1 h 0 1 + B 2 h 0 2 axm15-18 : δ in 1 , δ out 1 , δ in 2 , δ out 2 ∈ R axm19-22 : δ in 1 > 0 , δ out 1 > 0 , δ in 2 > 0 , δ out 2 > 0 axm23 : B 1 max(δ in 1 , δ out 1 ) + B 2 max(δ in 2 , δ out 2 ) ≤ ∆V max END Listing 15: 1 Controller 2 Tanks -Context MACHINE 1 C t r l _ 2 T a n k s REFINES A b s t r a c t T a n k SEES 1 C t r l _ 2 T a n k s _ C t x VARIABLES t , x s , h 1 , h 2 INVARIANTS i n v 1 : h 1 ∈ R → R i n v 2 : [0, t] ⊆ dom(h 1 ) i n v 3 : h 2 ∈ R → R i n v 4 : [0, t] ⊆ dom(h 2 ) i n v 5 : V = B 1 h 1 + B 2 h 2 INITIALISATION WITH V ′ : V ′ = B 1 h ′ 1 + B 2 h ′ 2 THEN a c t 1 : t := 0 a c t 2 : x s := Stable a c t 3 : h1 := {0 → h 0 1 } a c t 4 : h2 := {0 → h 0 2 } END
Initialisation is modelled in the same way as for the abstract system, replacing V by the two states h 1 and h 2 .

ctrl_transition_normal REFINES ctrl_transition_normal WHERE g r d 1 : B 1 h 1 (t) + B 2 h 2 (t) < V high g r d 2 : V low < B 1 h 1 (t) + B 2 h 2 (t) THEN a c t 1 : x s := Normal END ctrl_sense_too_high REFINES ctrl_sense_too_high WHERE g r d 1 : V high ≤ B 1 h 1 (t) + B 2 h 2 (t) THEN a c t 1 :
x s := Emptying END Listing 17: Abstract Tank -Transition and Sensing Discrete events. Listing 17 shows the transition and sensing refined events of the abstract tank model. This refinement follows the principle given in this section. It relies on substituting V with B 1 h 1 + B 2 h 2 using the gluing invariant.

Continuous events. Listing 18 shows the system's actuation. It is built following the method given in this section: abstract plant state V is replaced using the gluing invariant, and continuous predicates are updated in order to handle h 1 and h 2 (using two separate ODE) while retaining the exact same evolution domain.

A witness is provided for eq to establish event simulation. Note that the state of each valve (io 1 and io 2 ) of the two tanks are deduced from the system's state (s) using the TankModeChange predicate in grd2 of Listing 18, as defined in the preliminary study for this development (Section 6.3.1).

EVENT ctrl_actuate_pumps REFINES ctrl_actuate_pumps

ANY io 1 , io 2 , s , t ′ WHERE g r d 0 : t ′ ∈ R ∧ t < t ′ g r d 1 : Feasible([t, t ′ ], h 1 ⊗ h 2 , { ĥ1 ⊗ ĥ2 , ĥ′ 1 ⊗ ĥ′ 2 | solutionOf([t, t ′ ], ĥ′ 1 , ode(FlowODE(0, H 1,max , δ in 1 , δ out 1 , io 1 ), h 1 (t), t))∧ solutionOf([t, t ′ ], ĥ′ 2 , ode(FlowODE(0, H 2,max , δ in 2 , δ out 2 , io 2 ), h 2 (t), t))}, {h * 1 , h * 2 | V low < B 1 h 1 + B 2 h 2 ∧ B 1 h 1 + B 2 h 2 < V high }) g r d 2 : TankModeChange(s, io 1 , io 2 ) g r d 4 : s ∈ STATES g r d 5 : x s = s g r d 6 : V low ≤ B 1 h 1 (t) + B 2 h 2 (t) ∧ B 1 h 1 (t) + B 2 h 2 (t) ≤ V high WITH V ′ : V ′ = B 1 h ′ 1 + B 2 h ′ 2 eq : Solvable([t, t ′ ], eq, {V * | V low < V * ∧ V * < V high }) ∧ isFlowEq(s, [t, t ′ ], eq, 0, V max ) ∧solutionOf([t, t ′ ], B 1 h ′ 1 + B 2 h ′ 2 , eq) THEN a c t 1 : h 1 , h 2 :| t→t ′ solutionOf([t, t ′ ], h ′ 1 , ode(FlowODE(0, H 1,max , δ in 1 , δ out 1 , io 1 ), h 1 (t), t))∧ solutionOf([t, t ′ ], h ′ 2 , ode(FlowODE(0, H 2,max , δ in 2 , δ out 2 , io 2 ), h 2 (t), t)) &{h * 1 , h * 2 | V low < B 1 h 1 + B 2 h 2 ∧ B 1 h 1 + B 2 h 2 < V high } END
Listing 18: 1 Controller 2 Tanks -Actuation Event

Proofs

This model is associated with 70 proof obligations. They are mostly related to well-definedness (36%), because of the extensive use of theories in the model (both for continuous features and for the domain-specific tank features). POs relating to invariants (30%) are proven using the various results defined in the tank domain theories, and the remaining POs mainly come from refinement (28%) and feasibility (6%).

Guard strengthening is immediate, following the remarks of Section 6.2.2: it consists in substituting the abstract and the concrete continuous states using the gluing invariants. For other guards that do not use continuous state, the concrete model defines guards that are stricter than the guards of the abstract model. Guard strengthening proofs are then proven by substituting parameters and variables using the provided witnesses and gluing invariants, and by using the theorems defined in the theory of tanks.

According to Section 6.2.3, we notice that the simulation proof obligations (associated with the actuation event) boil down to establishing continuous predicate simulation (CPSIM). Unfolding the associated equation and filling its parameters, we obtain the following equation:

A ∧ I ∧ G∧V ′ = [0,t ′ ] B 1 h ′ 1 + B 2 h ′ 2 ∧ solutionOf([t, t ′ ], h ′ 1 , ode(Φ 1 ))∧ solutionOf([t, t ′ ], h ′ 2 ,ode(Φ 2 )) ∧ solutionOf([t, t ′ ], B 1 h ′ 1 + B 2 h ′ 2 , eq) ⇒ solutionOf([t, t ′ ], V ′ , eq) (4)
The witness provided for eq (solutionOf

([t, t ′ ], B 1 h ′ 1 + B 2 h ′ 2 , eq
)) constrains the equations of the concrete tanks to be "compatible" with the equations of the abstract tank. This allows to discharge the PO by substituting V ′ with B 1 h ′ 1 + B 2 h ′ 2 (using the witness for V ′ ). The expression of this witness is associated to a feasibility proof obligation: we are required to prove that there exists eq such that Equation 4 holds.

Many-to-Many Architectural Pattern

The many-to-many (M2M for short) architectural pattern corresponds to scenarios such as the one presented in Figure 24. These kinds of systems consist of several communicating controllers that are linked together via a network (internet, radio or other wireless means, etc.), each of which controls a plant. Compared to single-to-many systems where one controller is constantly aware of the state of every plant, in a many-to-many architecture, controllers only have direct access to their associated plant. Information on the other plants' state is supplied by other controllers, through the communication network. Such exchanges may generate imprecision (e.g. because of communication delays).

This imprecision must be taken into account when designing the system: controllers may have to take decisions depending on a global state, but this imprecision makes it difficult to establish such a global state accurately. This means that controllers must consider and anticipate potential incorrectness in the calculated state, and further constrain their behaviour.

Pattern Model

Like for the single-to-many pattern, we give the M2M pattern as a refinement. Similarly, we assume that the concrete machine only handles two continuous variables. Note that it can easily be extended to handle larger systems.

Machine States and Working Hypotheses

Let M A be a machine with discrete state x A s ∈ STATES A and continuous state x A p ∈ R → S A . Let M C be a refinement of M A consisting of two sub-components, i.e. two controllers, each being linked to one plant. The sub-components are modelled using two discrete states x C s,1 ∈ STATES C 1 and x C s,2 ∈ STATES C 2 and two continuous states

x C p,1 ∈ R → S C 1 and x C p,2 ∈ R → S C 2 .
Gluing invariant. Similarly to the S2M pattern, the gluing invariant between x A p and (x C p,1 , x C p,2 ) is of the form:

x A p = f (x C p,1 , x C p,2 ), with f ∈ S C 1 × S C 2 → S A .
Global continuous state estimation. In single-to-single systems, the controller has direct access to the plant's state (sensing is instantaneous). In the case of many-to-many systems, each controller is directly linked to one plant, but cannot sense the other plant's state directly and instantaneously. Instead, each controller sends its associated plant's state to the other controllers through a network, and retrieves through this network the state of the other parts of the system. This exchange unavoidably introduces imprecision, due to communication delay, rounding errors and so on. Consequently, controllers cannot access an exact state of the global system. Therefore, in order to maintain a global invariant on the system, each controller has to record a safe estimation of the state of the other components.

In practice, this is modelled using specific variables, x sim p,i , representing the estimation of the state of the remainder of the system. This state is assumed to be 1) regularly updated, such that the delay between its current value and the actual value of this state is bounded (i.e. bounded delay in the communication) 2) the controller is able to emulate the behaviour of this variable between two updates, meaning it is able to estimate the behaviour of the remainder of the system, using physics simulation, for example.

Concretely, Controller 1 is keeping track of variable x sim p,2 ∈ R → S C 2 that simulates Plant 2, and Controller 2 is keeping track of variable x sim p,1 ∈ R → S C 1 that emulates Plant 1.

Since communication delay is bounded, we assume that the difference between the estimation of the remainder of the state x sim p,i and its actual value x C p,i is bounded. We note ∆ sim i this bound, and we have:

∀i ∈ {1, 2}, ∀t * ∈ [0, t], ∥x C p,i (t * ) -x sim p,i (t * )∥ ≤ ∆ sim i
where ∥ • ∥ denotes a norm on the state space S C i . This bound depends on the specific properties of the network and of the physical phenomena models of the plants. It is usually provided in a specific theory of domains, formalising the application's domain knowledge.

Discrete state. Each controller of the concrete model has its own discrete state. This controller decides how its associated plant is controlled. However, at the abstract level, the defined abstract model describes a single discrete state only, the global state of the system. To ensure the consistency of the refinement of the abstract model, it is required to provide a gluing invariant, linking this abstract discrete global state to the concrete "local" discrete states, that correspond to the discrete state of each controller.

The relationship linking the local discrete states of each controller and global discrete state of the abstract controller is specific to each studied system; it defines how the local controllers behave, depending on the state of each other local controller.

In the following, this relationship is defined as a policy. It is modelled using a particular set predicate of possible relations between abstract and concrete discrete states. It is available in a given context or in a domain theory. The policy predicate of the form (x A s , x C s,1 , x C s,2 ) ∈ Policy establishes this relation. It is worth noticing that the concept of policy arises with the distributed, multi-controller nature of the system, encoded by the two distinct concrete discrete variables x C s,1 and x C s,2 . It is a way for the controllers to "agree" on a set of valid behaviours they shall follow. The definition of this predicate does not prevent from the checking of the refinement consistency as shown below.

Note that, policy is not explicitly defined in the single-to-many architectural pattern. Indeed, there exists only a single controller (equivalently, the policy predicate for a centralised controller is the identity:

x C s,1 = x C s,2 = x A s ).

Machine Header

MACHINE M A VARIABLES t , x A s , x A p INVARIANTS i n v 1 : t ∈ R + i n v 2 : x A s ∈ STATES A i n v 3 : x A p ∈ R → S A i n v 4 : [0, t] ⊆ dom(x A p ) MACHINE M C REFINES M A VARIABLES t , x C s,1 , x C s,2 , x C p,1 , x C p,2 , x sim p,1 , x sim p,2 INVARIANTS inv21-22 : x C s,1 ∈ STATES C , x C s,2 ∈ STATES C inv31-32 : x C p,1 ∈ R → S C 1 , x C p,2 ∈ R → S C 2 inv41-42 : [0, t] ⊆ dom(x C p,1 ) , [0, t] ⊆ dom(x C p,2 ) inv51-52 : x sim p,1 ∈ R → S C 1 , x sim p,2 ∈ R → S C 2 inv61-62 : [0, t] ⊆ dom(x sim p,1 ) , [0, t] ⊆ dom(x sim p,2 ) i n v 7 : ∀t * • t * ∈ [0, t] ⇒ ∥x C p,1 (t * ) -x sim p,1 (t * )∥ ≤ ∆ sim 1 ∧∥x C p,2 (t * ) -x sim p,2 (t * )∥ ≤ ∆ sim 2 i n v 8 : (x A s , x C s,1 , x C s,2 ) ∈ Policy i n v 9 : x A p = f (x C p,1 , x C p,2 )
Listing 19: M2M Pattern -Machine Header Listing 19 gives the header of both abstract and refined machines. The main point here is the correct definition of every variable used by the models, namely discrete (x A/C s ) and continuous (x A/C p ) states, as well as the variables used for emulating the global state (x sim p ). Following the discussion of Section 7.1.1, the behaviour of the variables is constrained using invariants. Invariant inv7 ensures that the emulated states do not drift too far from the actual states, and invariant inv9 is the gluing invariant linking the abstract and concrete continuous states. Invariant inv8 links the abstract and the concrete discrete states, using the Policy operator discussed above.

Initialisation for the machines is given in Listing 20. Variables are initialised as usual; note that we have chosen the simulating variables (x sim p,i ) to be equal to the exact ones.

END

Listing 20: M2M Pattern -Initialisation Because x A p and x A s disappear at refinement, witnesses have to be provided. They are based on the refinement's gluing invariants (inv9 and inv8, respectively).

Discrete Events

Sense A ANY s A , p A WHERE g r d 1 : s A ∈ P1(STATES A ) g r d 2 : p A ∈ P(STATES A × R × S A ) g r d 3 : (x A s → t → x A p (t)) ∈ p A THEN a c t 1 : x A s :∈ s A END Sense C 1 REFINES Sense A ANY s C 1 , p C 1 WITH s A , x A′ s : x A′ s ∈ s A ∧ (x A′ s , x C′ s,1 , x C s,2 ) ∈ Policy WHERE g r d 1 : s C 1 ∈ P1(STATES C ) g r d 2 : p C 1 ∈ P(STATES C × R × (S C 1 × S C 2 )) g r d 3 : (x C s,1 → t → (x C p,1 (t) → x sim p,2 (t))) ∈ p C 1 THEN a c t 1 : x C s,1 :∈ s C 1 END Sense C 2 REFINES Sense A ANY s C 2 , p C 2 WITH s A , x A′ s : x A′ s ∈ s A ∧ (x A′ s , x C s,1 , x C′ s,2 ) ∈ Policy WHERE g r d 1 : s C 2 ∈ P1(STATES C ) g r d 2 : p C 2 ∈ P(STATES C × R × (S C 1 × S C 2 )) g r d 3 : (x C s,2 → t → (x sim p,1 (t) → x C p,2 (t))) ∈ p C 2 THEN a c t 1 : x C s,2 :∈ s C 2 END
Listing 21: M2M Pattern -Sensing Events

Listing 21 shows the sensing event for the abstract and concrete machines. The key point is that the abstract sensing event is "split" in two events, one for each controller (Sense C 1 and Sense C 2 ). The main difficulty is to establish a correct relation between abstract and concrete discrete states. This is achieved using an adequate policy, that is used to express the witness for x A′ s and s A . Correct values must be provided for p C 1/2 to substitute p A . In particular, these concrete events are required to strengthen grd3.

Note that the transition event follows the same pattern, without the sensing predicate p (i.e. grd2 is removed).

Continuous Events

Listing 22 shows the actuation event for both systems. This actuation updates both the continuous state (x C p,1 and x C p,2 ) and the emulated state variable of each controller (x sim p,1 and x sim p,2 ).

Actuate A ANY P A , s , H A , t ′ WHERE g r d 0 : t ′ > t g r d 1 : P A ∈ (R + → S A ) × (R + → S A ) g r d 2 : Feasible(x A p , [t, t ′ ], P A , H A ) g r d 3 : s ⊆ STATES g r d 4 : x s ∈ s g r d 5 : H A ⊆ S A g r d 6 : x A p (t) ∈ H A THEN a c t 1 : x A p :| t→t ′ P A (x A p , x A′ p ) & H A END Actuate C REFINES Actuate A ANY P C 1 , P C 2 , s C 1 , s C 2 , x sim * p,1 , x sim * p,2 , H C , t ′ WHERE g r d 0 : t ′ > t g r d 1 : P C 1 ∈ (R + → (S C 1 × S C 2 )) × (R + → (S C 1 × S C 2 ))∧ P C 2 ∈ (R + → (S C 1 × S C 2 )) × (R + → (S C 1 × S C 2 )) g r d 2 : Feasible(x C p,1 ⊗ x sim * p,2 ⊗ x sim * p,1 ⊗ x C p,2 , [t, t ′ ], P C 1 × P C 2 ∩ { xp,1 , xsim p,2 , xsim p,1 , xp,2 | x sim p,1 = [t,t ′ ] x sim * p,1 , x sim p,2 = [t,t ′ ] x sim * p,2 }, H C ∩ { xp,1 , xsim p,2 , xsim p,1 , xp,2 | ∥ xp,1 -xsim p,1 ∥ ≤ ∆ sim 1 ∧ ∥ xp,2 -xsim p,2 ∥ ≤ ∆ sim 2 }) g r d 3 : s C 1 ⊆ STATES C ∧ s C 2 ⊆ STATES C g r d 4 : x C s,1 ∈ s C 1 ∧ s C s,2 ∈ s C 2 g r d 5 : x sim * 1 ∈ R → S C 1 ∧ [t, t ′ ] ⊆ dom(x sim * 1 ) g r d 6 : x sim * 2 ∈ R → S C 2 ∧ [t, t ′ ] ⊆ dom(x sim * 2 ) g r d 7 : H C ⊆ S C 1 × S C 2 × S C 1 × S C 2 g r d 8 : x C p,1 (t), x sim * p,2 (t), x sim * p,1 (t), x C p,2 (t) ∈ H C WITH x A′ p : x A′ p = f (x C′ p,1 , x C′ p,2 ) s A : (x A s , x C s,1 , x C s,2 ) ∈ Policy ∧ x A s ∈ s A THEN a c t 1 : x C p,1 , x sim p,1 , x C p,2 , x sim p,1 :| t→t ′ P C 1 (x C p,1 ⊗ x sim p,2 , x C′ p,1 ⊗ x sim′ p,2 ) ∧ P C 2 (x sim p,1 ⊗ x C p,2 , x sim′ p,1 ⊗ x C′ p,2 ) ∧x sim p,1 = [t,t ′ ] x sim * p,1 ∧ x sim p,2 = [t,t ′ ] x sim * p,2 &{ xC p,1 , xsim p,2 , xsim p,1 , xsim * p,2 | xC p,1 , xsim p,2 , xsim p,1 , xC p,2 ∈ H C ∧∥ xC p,1 -xsim p,1 ∥ ≤ ∆ sim 1 ∧ ∥ xC p,2 -xsim p,2 ∥ ≤ ∆ sim 2 } END Listing 22: M2M Pattern -Actuation Event
The continuous state is updated with two predicates, P C 1 and P C 2 , each of which relates to a continuous variable and the simulated continuous variable of the other (i.e. (x C p,1 , x sim p,2 ) and (x sim p,1 , x C p,2 )), thus effectively representing two separate and independent actuations, although they are executed simultaneously.

On the other hand, the functions associated to the simulated continuous variables are updated directly with functions (x sim * p,1 and x sim * p,2 ), which models the simulations managed and calculated by the controllers themselves. The predicate employed in the CBAP operator as well as in the Feasible predicate is the Cartesian product P C 1 × P C 2 , intersected with an additional predicate enforcing the assignments of x sim p,1 and x sim p,2 . Similarly, H A is substituted with H C , with the additional constraints that each continuous state variable simulation must remain close by ∆ sim i from the associated state variable's actual behaviour (i.e. ∥x C p,ix sim p,i ∥ ≤ ∆ sim i ). This additional constraint ensures the provided simulation functions are sufficient for the controller to behave correctly.

Witnesses are provided for s A and x A′ p , following the machine's gluing invariants. Note that we do not give witnesses for H A and P A ; this fact is discussed further in Section 7.2.

Proofs

The single-to-many architectural pattern yields multiple POs, mostly related to refinement. It is to be noted, again, that since it is a pattern, there is no general method for discharging all of these POs, since they rely on the specific features of the system.

In this section, we focus on invariant, guard strengthening and simulation POs, and we study how they are handled.

Invariant Preservation

The gluing invariant, linking abstract and concrete state variables, are preserved (PO 7 of Table 2b) with the use of witnesses. The discrete gluing invariant (inv8 in Listing 19) is proved with the help of witnesses for x A′ s and using the policy predicate. The continuous gluing invariant (inv9) is proved using the witnesses provided for x A′ p , that are based on the relation

x A p = f (x C p,1 , x C p,2 ).
For the preservation of the other invariants (PO 2 of Table 2a), typing and basic constraint invariants (invariants inv21-22 through inv61-62) are established using well-defined and well-constrained predicates. More importantly, invariant inv7 on the proximity of x p,i and x sim p,i is enforced by guard grd2 of the concrete actuation. In a later refinement, concrete values are provided for x sim p,i , and a guard strengthening PO is generated. It ensures that this concrete value satisfies the proximity constraint provided by the Feasible predicate (i.e. ∥ xp,ixsim p,i ∥ ≤ ∆ sim i ). The preservation of the other, system-specific invariants again depends completely on the nature of these invariants and of the concrete system's behaviour.

Guard Strengthening

Guard strengthening (see PO 6 in Table 2b) appears in particular in sensing events. It ensures that the concrete sensing can only occur when the abstract sensing is.

In concrete sensing event Sense C 1 for instance, the guard strengthening PO has the form:

A ∧ I∧(x A s , x C s,1 , x C s,2 ) ∈ Policy ∧ x A p = f (x C p,1 , x C p,2 ) ∧ ∥x C p,2 -x sim p,2 ∥ ≤ ∆ sim 2 ∧ (x C s,1 , t, (x C p,1 (t), x sim p,2 (t))) ∈ p C 1 ⇒ (x A s , t, x A p (t)) ∈ p A
The difficulty is to devise an updated guard (i.e. a value for p C 1 ) that allows to establish guard strengthening. In the particular case where the guard is of the form x A p ∈ pA (and (x C p,1 , x sim p,2 ) ∈ pC 1 ), we exploit the shape of the gluing invariant and the properties of x sim p,2 . We then have to find pC 1 such that:

(x C p,1 , x sim p,2 ) ∈ pC 1 ⇒ ∀x * p,2 • x * p,2 ∈ S 2 C ∧ ∥x * p,2 -x sim p,2 ∥ ≤ ∆ sim 2 ⇒ f (x C p,1 , x * p,2 ) ∈ pA
Indeed, if we have this property, x * p,2 is substituted with x C p,2 , and the gluing invariant is exploited to substitute f (x C p,1 , x C p,2 ) with x A p . This means that, to avoid missing the sensing of an event, the guard needs to take into account the simulation error bound ∆ sim 2 . Note that the constraints induced by the communication network and the continuous behaviours of the plants may entail a value of ∆ sim i for which the only correct value for pC is ∅, i.e. the only correct guard for the concrete event with regard to guard strengthening is ⊥. In this case, the system loses features (some concrete events are disabled).

For instance, if ∆ sim i is too big, it may be impossible to find a predicate pC strong enough to imply pA .

Simulation

As for the single-to-many pattern, this pattern generates simulation POs (see PO 5 in Table 2b), in particular associated with continuous events. A simulation proof obligation for the system's actuation (with unfolded CBAP) is written as:

A ∧ I ∧ G ∧ x A′ p = [0,t ′ ] f (x C′ p,1 , x C′ p,2 ) ∧ P C 1 (x C p,1 ⊗ x sim p,2 ,x C′ p,1 ⊗ x sim′ p,2 ) ∧ P C 2 (x sim p,1 ⊗ x C p,2 , x sim′ p,1 ⊗ x C′ p,2 )∧ ∀t * • t * ∈ [0, t ′ ] ⇒ ∥x C′ p,1 (t * ) -x sim′ p,1 (t * )∥ ≤ ∆ sim 1 ∧ ∥x C′ p,2 (t * ) -x sim′ p,2 (t * )∥ ≤ ∆ sim 2 ∧x C′ p,1 (t * ), x sim′ p,2 (t * ), x sim′ p,1 (t * ), x C′ p,2 (t * ) ∈ H C ⇒ P A (x A p , x A′ p ) ∧ ∀t * • t * ∈ [t, t ′ ] ⇒x A′ p (t * ) ∈ H A
This PO drives the design of P C i and H C , in a way similar to the single-to-many pattern, with the additional inclusion of the simulation error bound. Just like for guard strengthening, the idea is that these predicates shall be strict enough such that, even considering the possible gap between simulated and direct variables, simulation still holds.

Note that, for H C , the same technique as for guard strengthening is used. Guard strengthening is addressed when presenting the discrete events: by narrowing the bounds, we ensure that, despite the imprecision caused by the estimation of the global state, the tanks are safely controlled.

Simulation of the Event-B machines is ensured by the particular shape of the witnesses and witness feasibility proof obligations are generated.

Conclusion

The work presented in this paper formalises different hybrid system architectures in the form of a refinement pattern, allowing to introduce various structures as a development step. The resulting patterns are presented in the form of a refinement, to be applied for specific hybrid systems. These patterns are adaptable and useful, as they may be used at any point during the refinement chain, and can be composed to produce rich and complex architectures provided that the invariants gluing the abstract component and the components resulting from the decomposition hold. In addition, being presented under the form of a refinement, it is possible to use these patterns on a global system, or on one of its sub-components. This makes these patterns composable to incrementally produce rich and complex architectures.

Assessment

The proposed patterns have been applied to the case study of the control of a liquid volume level of a tank. The single-to-many pattern has been successfully applied to the case study of controlling the filling and emptying of two water tanks connected to a centralised controller. The many-to-many pattern has been applied to a similar case study, with two water tanks independently controlled by two controllers, communicating with bounded delay. The complete Event-B models for both cases studies are available at https://irit.fr/~Guillaume.Dupont/models.php.

In addition, these case studies also demonstrate the interest of providing domain theories that axiomatise the physics of the plants to be controlled. These domain theories encapsulate domain-specific knowledge related to tanks liquid level control, and in particular hypotheses issued from physics, and tanks and valves specific constraints (e.g. communication delay, volume computation according to the shape of the tanks, etc. ).

Note that one may consider, as a limitation of our approach, that the presence of only two tanks in our case study means that the presented patterns only allow to refine one abstract component with two concrete components. This is not the case as the presented patterns allow decomposition in more than two components by successive applications of the patterns. However, a direct instantiation of the patterns for an arbitrary number of components (greater than two) can be achieved using additional theories, in particular a theory of vectors.

Last, we mention that the many-to-many pattern can be seen as a model of a class of cyber-physical or autonomous systems, or in other words sets of hybrid systems that communicate with each other with decentralised control. However, such models require the availability of a constant to bound the communication delay between the controllers ensuring the whole system remains in a safe state. Computing this bounded delay is out of the scope of this paper.

Pattern-oriented design

Rather than designing an ad hoc hybrid system modelling language relying on Event-B we have chosen to rely on the definition of different formalised patterns on the one hand and on other domain theories on the other hand. Indeed, other patterns, like approximation and linearisation, in addition to the ones presented in this paper have been developed. Other domain theories axiomatising specific knowledge domains, in particular the knowledge related to the physics of the plants, have been defined. Examples of such domains are kinematics and oscillation behaviour. The obtained framework is depicted in Figure 35.

Proceeding in this way makes the proposed framework extensible and generic. Extensibility is ensured by the capability to introduce new formalised patterns, linked to the existing ones by a refinement relationship, and new relevant theories that may be required by the introduced patterns.

Use of this framework for the development of specific hybrid systems, requires first to define the domain theories needed to model the domain knowledge related to the specific system and the refinement chain that instantiates the corresponding patterns as shown at the bottom of Figure 35.

Perspectives

The work presented in this paper can be pursued in many directions. First, further studies on the many-to-many pattern can be carried out in order to support distributed control to guarantee global invariants deduced from the local invariants of each hybrid system taking part in the whole system. In particular, allowing the capability to add and/or remove a given component i.e. a hybrid system makes it possible to model dynamic systems and a sort of autonomy through this pattern. The definition of the timing analysis that provided the bound for communication is fixed as a constant in the current model. This value is issued from analysis of timing delays in the network of the communicating hybrid systems that is not explicitly described in the developed model.

Additional patterns may be defined in the framework, to handle other development operations, common in the design of hybrid systems. In particular, discretisation operations would allow to formally transform a continuous model of a hybrid system into a discrete one, closer to implementation, while ensuring the preservation of its properties. This operation could be further extended to handle floating-point numbers, as an approximated implementation of real numbers on real-world machines. Other types of approximations may be handled, for instance proportional-integrationderivation (PID), that addresses specific types of hybrid systems and are widely used in controller design.

Expanding on the idea of patterns and framework [START_REF] Dupont | An Event-B based generic framework for hybrid systems formal modelling[END_REF], it is possible to propose (formal) software product lines [START_REF] Beek | Towards modular verification of software product lines with mCRL2[END_REF][START_REF] Muschevici | Modular modelling of software product lines with feature nets[END_REF] dedicated to hybrid systems, further embedding design and verification. Event-B theories already make domain features reusable, and additional automations and reusable aspects may be envisioned, in particular on the proving side and on pattern instantiation. For instance, our work initiated in [START_REF] Dupont | Embedding approximation in Event-B: Safe hybrid system design using proof and refinement[END_REF][START_REF] Dupont | An Event-B based generic framework for hybrid systems formal modelling[END_REF] shows how Event-B refinement can be used to support approximation of hybrid models. This type of embedding may be used in the context of architectural patterns, to improve their usability, especially on the proof side.

Additional theories able to handle a larger panel of hybrid systems should be defined as well. For instance, in our work, we only handle ordinary differential equations (ODEs), which is the most common type of continuous behaviour models in hybrid systems; but other types of differential equations, together with their relevant properties, may be formalised in theories (e.g. partial differential equations). Regarding the specific hybrid systems, specific domain theories for physics may be defined, e.g. for kinematics, thermodynamics, fluid mechanics, etc. These theories are useful to design application-specific domain theories; for instance, theories for self-driving cars, trains, planes, and so on may be proposed to address several case studies in these respective domains.

Last, we would like to address the aspect of refinement feasibility and potential feature loss mentioned in Section 6.3.1. In fact, the situation we pointed out relates to a general problem of reachability on hybrid systems (i.e. both discrete and continuous state reachability). This problem is hard to tackle in Event-B. A domain-based approach would allow to give conditions on refinement feasibility for specific types of systems, but can hardly be generalised. Another possibility is to use hybrid model-checkers, particularly good at reachability analysis, to provide useful information on the consistency of the constraints of the system.

Figure 2 :

 2 Figure 2: Theories Overall Architecture

Figure 4 :

 4 Figure 4: Hybrid System Global Architecture

Listing 4 :

 4 Generic Transition and Sense EventsTransition. Transition events (corresponding to command arrow and the Ctrl box of Figure4) model internal changes in the controller. They represent user commands, internal timers or non-deterministic choices that occur in the discrete part of the system (mode automata). It updates the state of the automaton (act1 of Transition on Listing 4).

Figure 7 :

 7 Figure 7: Abstract Tank Model

  THEORY V a l v e s IMPORT RReal DATATYPES Status = ValveOpen | ValveClosed InOutValve = InOut( in_status : Status , out_status : Status) OPERATORS closeIn e x p r e s s i o n ( iov : InOutValve ) r e c u r s i v e d e f i n i t i o n c a s e s iov -InOut(i, o) ⇒ InOut(ValveOpen, o) . . . in_rstatus e x p r e s s i o n ( iov : InOutValve ) r e c u r s i v e d e f i n i t i o n c a s e s iov -InOut(ValveOpen, o) ⇒ 1.0 -InOut(ValveClosed, o) ⇒ 0.0 InOutPossible e x p r e s s i o n ( ) d i r e c t d e f i n i t i o n {InOut(ValveOpen, ValveOpen), . . .} . . . THEORY Flow IMPORT V a l v e s , D i f f E q DATATYPES TankState = Stable | Emptying | Filling | Normal OPERATORS isFlow p r e d i c a t e ( s : TankState , D : P(R) , Φ : R → R , Q min : R , Q max : R ) w e l ld e f i n e d n e s s D ⊆ dom(Φ) r e c u r s i v e d e f i n i t i o n c a s e s s -Stable ⇒ constant(D, Φ) -Emptying ⇒ decreasing(D, Φ) ∧ Q min ≤ Φ ≤ Q max . . . isFlowEq p r e d i c a t e ( s : TankState , D : P(R) , e : DE(S ) , Q min : R , Q max : R ) w e l ld e f i n e d n e s s Solvable(D, e) d i r e c t d e f i n i

  FlowODE e x p r e s s i o n ( Q min : R , Q max : R , δ in : R , δ out : R , io : InOutValve ) w e l ld e f i n e d n e s s 0 < Q min , 0 < Q max , δ in > 0 , δ out > 0 d i r e c t d e f i n i t i o n . . . TankModeChange p r e d i c a t e ( state : TankState , io 1 : InOutValve , io 2 : InOutValve ) d i r e c t d e f i n i t i o n . . . Listing 6: Valves and Flow Domain Theories

Figure 9 :

 9 Figure 9: Single-to-single Pattern Typical Scenario

Figure 14 :

 14 Figure 14: Single-to-many Pattern Typical Scenario

Figure 19 : 1

 191 Figure 19: 1 Controller, 2 Tanks Configuration

•

  emptying mode: input pumps closed (In i = 0), output pumps open (Out i = 1); • filling mode: input pumps open (In i = 1), output pumps closed (Out i = 0); • stable mode: every pump closed (In i = Out i = 0); • normal mode: pumps are closed or open.

Listing 16 : 1

 161 Controller 2 Tanks -Machine Header

Figure 24 :

 24 Figure 24: Many-to-many Pattern Typical Scenario

Figure 35 :

 35 Figure 35: Framework Tools -Architectural Patterns

Table 1 :

 1 Model structure

Context (Table

1

.a). Context is a modelling component for describing the static properties of a system. It includes the definitions, axioms and theorems needed to describe the required concepts using elementary components such as Carrier sets s, constants c, axioms A and theorems T ctx .

Table 2 :

 2 Proof Obligations

  V high -B 1 ∆ sim 1 ≤ B 1 h sim 1 (t) + B 2 h 2 (t) THEN a ct 1 : x 2 s := Emptying END Listing 26: 2 Controllers 2 Tanks -Sensing Events EVENT ctrl_actuate_pumps REFINES ctrl_actuate_pumps ANY s 1 , s 2 , t ′ , io 1 , io 2 , h sim *

	ctrl_sense_too_high_1 REFINES ctrl_sense_too_high	ctrl_sense_too_high_2 REFINES ctrl_sense_too_high
	WHERE	WHERE
	g r d 1 : V high -B 2 ∆ sim 2 ≤ B 1 h 1 (t) + B 2 h sim THEN 2 (t)	g r d 1 :
	a c t 1 : x 1 s := Emptying
	END

Notation. The superscripts A and C denote abstract and concrete features.

We first introduce a set of continuous features, aimed at modelling continuous behaviour in Event-B models. Second, these features are used to define a generic model, formalising an abstract and generic model of controller-plant loop hybrid systems. The derivation of specific hybrid system models from this model is achieved by refinement.Note that our intention with the framework is to build it on core Event-B, which means we do not change the semantics or the language of Event-B; we simply use theories to gather and factorise higher level constructs. Our approach can be seen as low-level modelling.

 [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]This work was supported by grant ANR-17-CE25-0005 (The DISCONT Project https://discont.loria.fr) from the Agence Nationale de la Recherche (ANR).

Application to the Case Study

In this section, we propose another refinement of the abstract tank, corresponding to the many-to-many architectural pattern presented in this section. It models a system consisting of two tanks of definite shape, each controlled by an independent controller. Figure 29 gives the typical configuration of the system to be designed.

The core of the system is close to the S2M (1 controller 2 tanks) system designed in Section 6.3. It consists of two cylinder tanks with known bases and maximum heights, and the controller accesses the height of liquid in the tank rather than the direct volume (that is calculated). The behaviour of the pumps is identical to that of the S2M case study.

Contrary to the S2M case study where one controller controls several plants (centralised control with the capability to build a global state of the controlled plants), the goal of this refinement is to model a situation where each tank is equipped with a controller, and both controllers communicate with each other through a communication network with a bounded delay time.

The difficulty of this development is the computation of a global state (ideal case) or of a safe estimation of a global state, despite the latency of the network and the error that it generates; this is the main use of the many-to-many architectural pattern with distributed control.

Preliminary Study

Plant description. The plant is exactly the same as for the single-to-many case study (see Section 6.3.1: two cylinder tanks of bases B 1 and B 2 and maximum height H 1,max and H 2,max , containing a height of liquid h 1 (t) and h 2 (t) and connected to pumps of fixed flow (δ in/out 1/2 ). Consequently, the gluing invariant and the equations used in the model are identical to the S2M case.

Note that, in terms of pattern application, we again have

Controller description. The controllers for this system are more complex than for the S2M case study. The system consists of two controllers, each of which is able to control the pumps and sense the height of liquid in one tank.

The controllers communicate with each other and exchange their current (discrete and continuous) states. The communication is delayed by an arbitrary time, that is assumed to be bounded.

In addition to the pumps they control, and in order to maintain a global safety invariant, each controller sees a global state, or a safe approximation of it. For that, it estimates the continuous state of the other controller, basically by emulating it using knowledge of its behaviour and the information it gets from the network. Thus, controller 1 keeps track of the emulated height of tank 2 (h sim 2 ) and similarly controller 2 keeps track of the emulated height of tank 1 (h sim 1 ). We assume that, at any given point, the difference between the real height and the simulated height is bounded by a constant, that basically encompasses the simulation errors and the network's delay:

Note that no additional assumption is made on how the controller calculates h sim i .

Finally, each subsystem has its own discrete state, taken in the TankState type (i.e. STATES C 1 = STATES C 2 = STATES A = TankState). These states together with the discrete state of the abstract machine are linked via the Policy set, that is left abstract in this development. Note that, in practice, any policy may be proposed, provided it is compatible with the system's invariants. For example, the policy can be defined based on the principle of keeping each tank level of liquid close to the average.

Requirements. The goal of the system is, as for the abstract one, to keep the global volume (B 1 h 1 + B 2 h 2 ) within the bounds V low , V high . The requirements are enriched to reflect the particular architecture of the system:

ENV3 each tank is controlled independently by communicating controllers; communication introduces bounded delays and errors, encapsulated in a constant, ∆ sim i , for each controller i.

Refinement feasibility. Like for the single-to-many tank control case study, the physical properties of the tanks (base and maximum height) may induce a system that cannot be safe, or that may be too constrained, and misses relevant possible behaviours. As discussed in the preliminary study for the single-to-many case study (Section 6.3.1), it is required that the total maximum volume of the tanks Vmax is greater than the lower bound for the volume V low , or possibly greater than the higher bound for the volume to avoid loosing capabilities. We recall that other operators are found in the tank theories (see Section 4.2).

Machine header. Listing 24 shows the machine's header and initialisation. Note that, as a matter of readability, we often give the invariants of one of the controllers; the others are abbreviated with dots and can be obtained by switching the indexes.

A big part of the header (inv1-12 and inv17-18) is dedicated to define the numerous variables together with their associated types and basic properties. In particular, inv9-12 ensure that the height of liquid in each tank (x C p,i ), as well as their emulated (approximated) counterparts (x sim p,i ), is bounded by 0 and H i,max . Invariants inv13-14 encode the properties of the simulated variables (h sim i ), that must not drift away too far from their real counterpart.

Listing 24: 2 Controllers 2 Tanks -Machine Header inv15-16 give an additional interesting properties, built on the principle explained in Section 7.2.2. The idea is that, if the estimated volume, despite the potential error ∆ sim i is in the bounds, then the actual volume is as well. Finally, inv19 and inv20 encode the gluing invariant of this refinement, for the continuous and discrete states, respectively.

In addition to this header, the initialisation is straightforward: both sub-components are in stable mode with a given initial amount of liquid inside. The emulated variables receive the same initial value as a starting point (but could also get another value provided it does not violate the invariants). A witness is provided for the substituted variables, following the gluing invariant. Discrete events. Listing 25 presents two transition events of the machine. Following the pattern, they are duplicates of the abstract ctrl_transition_normal transition event, and each event references only the variables of one controller at a time.

Following the remarks on guard strengthening, we need to ensure that, even if the emulated variables are the furthest allowed by their real counterpart, the guard is still at least as strong as the abstract one. Note that:

we have h sim 2 (t) + ∆ sim 2 ≥ h 2 (t) and deduce:

We proceed symmetrically for controller 2 and for the other predicate (with V low ).

For the record, we give the sensing events of the machine (Listing 26). They are constructed in the same way as the transition events, and following the methodology of the many-to-many architectural pattern given in this section.

Listing 27: 2 Controllers 2 Tanks -Actuation Event Continuous events. Listing 27 shows the system's actuation, built from the concepts presented in the single-to-many pattern case study, but following the many-to-many architectural pattern. The goal of this actuation is to update the behaviour of the two continuous states and two emulated continuous states, according to the current discrete state of each controller.

The evolution domain ensures that the estimated global volume remains within the bound, including the allowed, bounded imprecision.

A witness is given for eq, the same as for the single-to-many case study, so that we can establish simulation. Note that the functions associated with the emulated variables are not given explicitly; the way they are calculated could be specified in a later refinement (linear/polynomial approximation, stochastic models, etc.).

Proofs

This model is associated with 153 POs in total, most of which are related to well-definedness (27%) of the use of the operators defined in the theories and to invariants (47%), and in particular typing invariants. The other POs relate to refinement mainly (21%), and to feasibility of actions and witnesses (5%).