Ph.D. thesis presented by Thao Dang, speciality Automatic Control, VERIMAG, Advisor Oded Maler.
Manuscript (in English, 192p),
report
(in French), Slides of my presentation (in
English).
The lack of methods for computing reachable sets of continuous dynamics has been the main obstacle towards an algorithmic verification methodology for hybrid systems. Unlike the conventional approaches which attempt to find exact solutions and are thus limited by undecidability of most non-trivial systems, our approach is based on an efficient method for representing sets and a combination of techniques from simulation, computational geometry, optimization, and optimal control. We develop two effective approximate reachability techniques for continuous systems: one is specialized for linear systems and extended to systems with uncertain input, and the other can be applied for non-linear systems. Using these reachability techniques we develop a safety verification algorithm which can work for a broad class of hybrid systems with arbitrary continuous dynamics and rather general switching behavior.
We next study the problem of synthesizing switching controllers for hybrid systems with respect to a safety specification. A safety specification is specified as a subset of the state space within which the system must remain. We present an effective synthesis algorithm based on the calculation of the maximal invariant set and the approximate reachability techniques.
Another, not less important, goal of this thesis is to develop a working tool for analyzing hybrid systems. We have implemented most of the algorithms presented in this thesis in the tool d/dt. The current version of the tool deals with hybrid systems with linear differential inclusions and provides automatic safety verification and controller synthesis. Besides numerous academic examples, we have successfully applied the tool to verify some practical systems.
Keywords: Hybrid automata, differential equations, reachability analysis, algorithmic verification, controller synthesis
Le manque de méthodes de calcul des ensembles atteignables des
dynamiques continues est l'obstacle principal vers une méthodologie
algorithmique de vérification. Nous développons deux
techniques approximatives d'analyse d'atteignabilité pour les systèmes
continus définis par des équations différentielles
ordinaires. Ces techniques sont basées sur une méthode efficace
pour représenter des ensembles et une combinaison des techniques
de la simulation, de la géométrie algorithmique, de l'optimisation
et de la commande optimale. La première technique est spécialisée
pour les systèmes linéaires et étendue aux systèmes
avec entrée incertaine, et la seconde peut être appliquée
aux systèmes non-linéaires. En utilisant ces techniques d'analyse
d'atteignabilité nous développons un algorithme de vérification
de propriétés de sûreté qui peut être
appliqué à une large classe des systèmes hybrides
(avec des dynamiques continues arbitraires et des dynamiques discrètes
assez générales).
Nous étudions ensuite le problème de la synthèse de contrôleurs de sûreté pour les systèmes hybrides. Une propriété de sûreté est spécifiée par un sous-ensemble de l'espace d'état dans lequel le système doit rester. Nous présentons un algorithme de synthèse de contrôleurs par commutation basé sur le calcul de l'ensemble maximal d'invariance et les techniques d'analyse d'atteignabilité.
Nous avons implanté la plupart des algorithmes développés dans un outil expérimental. La version courante de l'outil peut traiter les systèmes hybrides avec les inclusions différentielles linéaires et permet deux types d'analyses automatiques : la vérification de propriétés de sûreté et la synthèse de contrôleurs de sûreté. En dehors de nombreux exemples académiques, nous avons appliqué avec succès l'outil pour analyser quelques systèmes pratiques.
Mots-clés : automates hybrides, équations différentielles,
analyse d'atteignabilité, vérification formelle, synthèse
de contrôleurs