key: cord-0043680-cv2vph45
authors: Afendi, Meryem
title: A Correct by Construction Approach for the Modeling and the Verification of Cyber-Physical Systems in Event-B
date: 2020-04-22
journal: Rigorous State-Based Methods
DOI: 10.1007/978-3-030-48077-6_31
sha: cc56a7cd7986a99703b07e3a1f3b684749696830
doc_id: 43680
cord_uid: cv2vph45

Cyber-Physical Systems (CPSs) connect the real world to software systems through a network of sensors and actuators: physical and discrete components interact in complex ways by involving different spatial and temporal scales. One of the most common architectures for CPSs is a discrete software controller which interacts with its physical environment in a closed-loop schema where input from sensors is processed and output is generated and communicated to actuators. We are concerned with the construction and verification of the correctness of such discrete controller using a correct by construction approach, which requires correct integration of discrete and continuous models.

In CPSs [1] , the measurement of continuous behaviors is performed by sensors. Ideally sensors have a continuous access to these measurements, which can be captured by an abstract model of CPSs, called Event-Triggered system by Kopetz in [2] . However, implementing such models is difficult in practice. Therefore, an approach to develop CPSs is to introduce a more realistic model called Time-Triggered system where sensors take periodic measurements [2] . Contrary to Event-Triggered models, properties on Time-Triggered models are difficult to verify since their controllers are discrete. Platzer et al. [3, 4] use this approach to model hybrid systems, which represent the most common mathematical models for CPSs. They have proved that a Time-Triggered model is a refinement of an Event-Triggered model, by using hybrid programs (HPs) [3] and an extension of the differential dynamic logic (dL), called the differential refinement logic (dRL). In addition to dL formulas, dRL introduces formulas of the form α ≤ β, α refines β, with α and β denoting HPs. However dRL is not supported by any prover and dRL formulas can only be manually proved, which heavily restricts its use, especially in an industrial context. This is why we propose the development of an approach that takes advantage of dRL and applies the reasoning of HPs in Event-B [5] , a formal method based on set theory, first-order logic and predicate logic.

The development of techniques and tools to effectively design hybrid systems has drawn the attention of many researchers [6] [7] [8] [9] [10] . Traditional approaches are based on simulation tools like Matlab/Simulink [11] . Since these tools are timeconsuming and produce results tainted with uncertainty, these approaches can be very expensive and difficult to apply. To overcome these limitations, several formal approaches, which can be grouped into two categories, have been proposed: model-checking-based approaches [6, 7] and proof-based approaches [3, [8] [9] [10] , have been proposed. Proof-based approaches use deductive verification to prove the properties of hybrid systems. One of the strong points of these approaches is that they support the description of any kind of hybrid systems. However, they require significant effort and a high expertise in modelling and proof phases. A. Platzer introduced in [3] a first-order dynamic logic in the domain of real (IR), called dL, to specify hybrid systems and verify their correctness using its associated proof calculus. The major advantage of this logic is its ability to handle differential equations, even those with non-polynomial solutions. Moreover, dL and its associated proof calculus are supported by two automatic formal verification tools, KeYmaera and its successor KeYmaera X [12] . In [10] , Dupont et al. introduced a proof-based approach to model and prove hybrid systems in Event-B. They use the Theory plug-in of Event-B to define theories that handle continuous aspects of hybrid systems such as differential equations. The behavior of CPSs is specified by three Event-B models: System model that is used to describe the continuous evolution of the physical part, State-System model that refines the previous model by adding the evolution of the discrete part (the controller) and Controlled-System model that refines State-System model by adding the interaction between the physical part and the discrete part.

Our work is supported in part by the DISCONT project [13] funded by the French National Research Agency (ANR). The objective of this project is to elaborate a correct-by-construction method, based on Event-B, to specify hybrid systems models. Two approaches are considered. The first one, developed by Dupont et al. [10] , is based on a translation of hybrid automata in Event-B. In our approach we propose to model the high-level structure of hybrid programs in Event-B, and more precisely the generic templates defined for modelling Event and Time-Triggered systems in dRL to take advantages of its proof obligations. To handle continuous aspects of hybrid systems in Event-B, we use the abstract model System of Dupont et al. as a starting model, as well as their theories developed to handle differential equations and continuous functions. To validate our approach, we chose the Stop Sign case study [14] which deals with a stop sign controller whose objective is to ensure the stopping of a car before a stop signal SP . In this case study, the differential equation that represents the evolution of the physical part is linear and can be easily solved. To handle more difficult differential equations we plan to integrate an external mathematical tool as a back-end tool in Event-B associated tools. So far, our approach has focused on the most abstract level of hybrid systems design where all transitions are instantaneous, that is, duration issues are not considered. It consists of three models (see Fig. 1 ). Event-Triggered model (EventTriggered Ctx and EventTriggered M of Fig. 1) is a generic abstract model designed to specify and prove systems with continuous controllers in Event-B. It defines a formula saf e used in dRL to represent the system's safety envelope. To model the alternation between the controller and the physical part as represented in HPs ((ctrl; plant) * , where ctrl denotes the discrete evolution, followed by the continuous evolution plant), Event-Triggered model defines a variable exec that can take two values ctrl and plant. In Event-B, the time must be explicitly handled. To be sure that this explicit time will only be updated after the execution of the controller, we added another value, prg, to exec. Therefore, our model follows the following structure: init; (ctrl; plant; prg) * .

To model Time-Triggered systems in Event-B, we designed a new model, named Time-Triggered (TimeTriggered Ctx and TimeTriggered M of Fig. 1) , that refines the previous one. The sensors of such systems take periodic measurements of physical state variables and the longest time between these sensors updates is bounded by a symbolic duration . For this purpose, Time-Triggered model defines a variable d to know whether the duration is reached or not. Since the controller of such systems must make a choice that will be safe for up to time, we replaced the formula saf e by a new safety envelope named saf eEpsilon that depends on both the current discrete state and the time duration , in addition to the current physical state. Finally, to prove that TimeTriggered M refines EventTriggered M, we establish that, during a control period , saf eEpsilon implies saf e. Moreover, we must guarantee that the continuous controller is able to execute exactly when saf e is no longer satisfied. In addition, in the Time-Triggered model, we must also guarantee that the system will not exceed the domain of the safety envelope within time .

As future work, we plan to integrate Mathematica [15] , a symbolic mathematical computation system that resolves differential equations, as a back-end tool in the Rodin platform to resolve differential equations. We also plan to define a refinement of the Time-Triggered model to take into account duration between the sending of continuous measurements by sensors and their processing by the controller as well as duration between the sending of actions by the controller and their execution in order to get a model that corresponds better to real CPSs, and consequently implements this concrete model.

Cyber physical systems: design challenges

Event-triggered versus time-triggered real-time systems

Differential dynamic logic for hybrid systems

Differential refinement logic

Modeling in Event-B: System and Software Engineering

HyTech: a model checker for hybrid systems

PHAVer: algorithmic verification of hybrid systems past HyTech

Practical theory extension in Event-B

Core hybrid Event-B I: single hybrid Event-B machines

Proof-based approach to hybrid systems development: dynamic logic and Event-B

A toolbox for simulation of hybrid systems in Matlab/Simulink: Hybrid equations (HyEQ) toolbox

KeYmaera X: an axiomatic tactical theorem prover for hybrid systems

How to model and prove hybrid systems with KeYmaera: a tutorial on safety

The Mathematica, 5th edn. Wolfram Media