Embedding Approximation in Event-B: Safe Hybrid System Design Using Proof and Refinement

Hybrid systems consist of a discrete part (controller) that interacts with a continuous physical part (plant). Formal verification of such systems is complex and challenging in order to handle both the discrete objects and continuous objects, such as functions and differential equations for modelling the physical part, for synthesising hybrid controllers. In many cases, where the continuous component model uses complex differential equations, a well-defined approximation operation involves simplifying it. The aim of this approximation is to ease the development of the controller, which would not be feasible with the actual differential equation. We claim this approximation operation can be treated as an extension of the discrete refinement operation, as long as all the necessary mathematical concepts are formalised. This paper extends the Event-B’s refinement which is capable of expressing an approximation between two hybrid systems as a refinement relation. We encode this approximate refinement relationship in Event-B, relying on its deductive reasoning enhanced by the theory of approximation based on the notion of approximate (bi-)simulation. New proof obligations resulting from this approximate refinement are highlighted. Finally, we illustrate how it applies to a case study borrowed from literature.