OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

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

Dupont, Guillaume. Correct-by-Construction Design of Hybrid Systems Based on Refinement and Proof. PhD, Informatique et télécommunication, Institut National Polytechnique de Toulouse, 2021

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


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

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Laboratory name:
Research Director:
Aït-Ameur, Yamine and Singh, Neeraj Kumar
Deposited On:24 Aug 2021 14:21

Repository Staff Only: item control page