Formalizing Hybrid Systems Using Event-B:Theory And Practice

Nowadays, hybrid systems are very important in the development of embedded systems. In such systems, a piece of software, the controller, is supposed to manage an external situation, the environment. The controller works in a discrete fashion in that it is triggered regularly by detecting the status of the environment (using some sensors), and then reacts by sending some information to the environment (using some actuators). Between two successive controller detections and actions, the environment is evolving in a continuous way. The design of a controller that correctly matches the physical environment has become a challenge.Various scientific community have contributed with their own approaches to this area:computer science, control, and modeling and simulation communities. We mainly place ourselves in the computer science community, but we also have some connections with the control community, and the modeling and simulation community.Other works in computer science community mainly focus on software verifica-tion, here we would like to propose an approach that certainly focus on verification, but also on modeling, simulation, and proof. Our purpose is to construct hybrid systems in a correct fashion. More precisely, based on Event-B, we propose a top-down approach that supports the development of hybrid systems from requirements down to final development. For this, our con-struction is based on successive refinements, allowing the development to be done in a gradual fashion. In the development of hybrid system, we concentrate on the following key issues:well-defined requirement document and refinement strategy, modeling, refinement, proving, and simulation.Here are the main contributions of this thesis:(i) Methodology Contribution Based on Event-B, requirement document and refinement strategy need to be first defined before formal modelling. We insist a lot on the importance of writing a well defined requirement document and a careful refinement strategy. Before modeling, the refinement strategy is used to define clearly how the requirements can be gradually taken into account in successive refinements. It also helps us to trace the formal development back to the requirement document, and check whether we have taken all requirements into account. To achieve this, we propose some rules for defining the requirement document and the refinement strategy,(ii) Theoretic Contribution We explain how hybrid systems with time function can be developed in Event-B and we show how we can transform a discrete approach to a continuous one. This is based on the usage of refinement. In order to support complex physical system, we extend the approach of model-ing hybrid systems with a new one called "Click":this constitutes a systematic design pattern for the time feature of hybrid systems. For those hybrid systems where the continuous parts are defined by differential equations, we try to give a theoretical approach on how to prove properties of differential equations without solving them. This work is based on solid mathematic foundations:the usage of Euler approximations and that of non standard analysis,(iii) Practical Contribution This study contains many practical examples whose role is to explain our approach. Such examples cover nuclear cooling control, train control, aircraft collision avoidance, water tank, etc. We believe that examples are important to show that this approach to hybrid systems can be made practical. In order to improve the confidence in formal modeling, we also propose some complementary approaches for hybrid system development. This includes the usage Simulink and animation, the introduction of sensor and actuator pat-terns, and an implicit invariant discovery approach as well.(iv) Software Contribution In order to complement formal development and translate Event-B model to Simulink model, we developed a plug-in for the Rodin platform. This plug-in can perform this translation automatically.