Correct-by-Construction Design of Hybrid Systems Based on Refinement and Proof

摘要

Hybrid systems are a wide category of systems consisting of multiple computers, linked together by some means and interacting with physical devices. Usually cheap, adaptable and incredibly versatile, these systems rapidly found their place in our everyday life, and can be found in basic devices like smart light bulbs, or in more complex structures such as smart factories or autonomous vehicles. In particular, due to their numerous advantages, they can nowadays be found in safety-critical domains, including avionics, self-driving cars or energy distribution. The complex and hybrid nature of hybrid systems make them quite hard to design in a safe way: while computer science is mostly able to deal with their discrete parts and control theory with their continuous part, we lack some kind of formalism that would be able to deal with both of these aspects and their integration with one another. The formal modelling of safety-critical hybrid systems is thus a major challenge of the domain. To overcome this challenge, we propose a generic formal framework, aimed at safely modelling hybrid systems in a correct-by-construction fashion, inherited from the Event-B method the framework is based on. This framework takes the form of an extensive set of theories that expands Event-B with mathematical features necessary to model continuous behaviours (e.g. continuous functions and differential equations), a generic model that encodes a generic hybrid system, complete with its controller and continuous plant, and a series of patterns, based on refinement, that allow to ease the design process. In particular, we defined three formal patterns, inspired by general practice in hybrid system designs: approximation (substituting an equation system with an approximately equivalent one), centralised control with multiple plants (splitting a plant into a set of plant with a centralised controller) and distributed hybrid systems (system made of components that each consist of a controller and a plant, enforcing a global invariant). This framework is designed to be extensible: adding a new component is done by describing it as a refinement of the generic model, and possibly to accompany it with relevant theories. We used our framework on various problems taken from control theory, including computer-assisted cars, water tanks, robots and inverted