Doctorant sous la direction de A. Girard

Titre de la thèse: Reachability Analysis of hybrid systems for verification and synthesis of cyber-physical systems
Résumé de la thèse: Models of cyber-physical systems are heterogeneous by nature: discrete dynamic systems for computations and continuous differential equations for physical processes. We will focus on physical processes described by linear differential equations. The first part of the work will consist in modeling of design contracts using hybrid automata. The second part of the work will deal with the development of reachability algorithms specific to the resulting models which will allow us to compute of (an approximation of) the set of all possible trajectories of the CPS for all admissible initial conditions and disturbances. The developed algorithms will then be used to solve the following problems related to verification and synthesis of cyber-physical systems: Verification of contracts: given a controller, a contract for its implementation, verify that all trajectories of the closed loop cyber-physical system satisfy a set of specifications (typically formulated as safety properties, stability or a certain level of performance with respect to some metrics). Synthesis of contracts: given a controller and a set of specifications for the behavior of the closed loop system, synthesize a suitable contract for the implementation of the controller. Co-synthesis of controller and contract: given a set of specifications, synthesize a controller and a contract for its implementation. These problems can be reformulated, respectively, as verification, parameter synthesis and controller synthesis for hybrid systems for which we will develop solutions based on our reachability analysis techniques. A toolbox compiling the different algorithms will be developed.