Guaranteed properties of dynamical systems under perturbations
Analyses formelles des propriétés des systèmes dynamiques sous perturbations
Résumé
Since dynamical systems has a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems in order to guarantee their correct functioning. Nevertheless, computing such type of system has never been an easy task, as the complexity of these systems is constantly increasing, in addition to the perturbations that may arise during their performance, as well as undefined parameters that may exist. To ensure that a system always produces the expected results and does not fail in any way, a formal verification of its behavior and properties is necessary.In this thesis, we study dynamical systems from different aspects and using various techniques. More specifically, we focus on the formal verification of some of its critical properties such as schedulability, synchronization, robustness and stability.In the first part, we start with the formal verification of real-time systems under uncertainty, where we use parametric timed automata sometimes extended by stopwatches to model systems with preemption. This formalism is very suitable for real-time systems due to its good expressiveness. It allows to study the schedulability of the flight control of a space launcher with unknown parameters and under constraints. Then, a synthesis of the admissible timing values of the unknown parameters is provided by a parametric timed model checker. We increase the complexity of the problem by taking into consideration the switch time between two threads. We extend this work by developing a tool that translates a given real-time system design into parametric timed automata in order to infer some timing constraints ensuring schedulability.In the second part, we study the stability of dynamical systems and the robustness of controls.We give a simple technique based on Euler's integration method which allows to build an invariant set around a given system. This technique guarantees that the approximate Euler solutions are attracted by a limit cycle. We apply the method on different systems, including chaotic systems with strange attractors. Furthermore, we show that a basic combination of a random sampling with a symbolic computation method assists to deal with robust control problems for nonlinear systems. Also, we illustrate a basic condition guaranteeing that a system with perturbation is robust under a repeated control sequence obtained by solving a horizon optimal control problem. Finally, we unified the main contributions of the second part in a tool called ORBITADOR which checks the stability of a given system and notably returns plots containing the evolution of the system in different views and the shape of the invariant if it exists
Étant donné que les systèmes dynamiques ont un impact majeur sur le développement humain, en particulier les systèmes critiques qui peuvent mettre des vies humaines en danger en cas de problème. D'où la nécessité d'étudier le comportement de ces systèmes afin de garantir leur bon fonctionnement. Néanmoins, le calcul de ce type de système n'a jamais été une tâche facile, puisque la complexité de ces systèmes est toujours en augmentation, en plus des perturbations qui peuvent survenir lors de leur fonctionnement, ainsi que des paramètres indéfinis qui peuvent exister. Pour s'assurer qu'un système produit toujours les résultats attendus et n'échoue en aucune façon, une vérification formelle de son comportement et de ses propriétés est nécessaire. Dans cette thèse, nous étudions les systèmes dynamiques sous différents aspects et en utilisant diverses techniques. Plus précisément, nous nous concentrons sur la vérification formelle de certaines de ses propriétés critiques telles que l'ordonnancement, la synchronisation, la robustesse et la stabilité. Dans la première partie, nous commençons par la vérification formelle de systèmes temps réel sous incertitude, où nous utilisons des automates temporisés paramétrés parfois étendus par des "stopwatches" pour modéliser des systèmes avec préemption. Ce formalisme est très adapté aux systèmes temps réel en raison de sa bonne expressivité. Il permet d'étudier l'ordonnancement de la commande de vol d'un lanceur spatial avec des paramètres inconnus et sous des contraintes. Ensuite, une synthèse des valeurs temporelles admissibles des paramètres inconnus est fournie par un model checker paramétré temporisé. Nous augmentons la complexité du problème en prenant en considération le temps de basculement entre deux threads. Nous étendons ce travail en développant un outil qui traduit une conception de système temps réel donnée en automates temporisés paramétrés afin d'inférer des contraintes temporelles assurant l'ordonnancement. Dans la deuxième partie, nous étudions la stabilité des systèmes dynamiques et la robustesse des commandes. Nous donnons une technique simple basée sur la méthode d'intégration d'Euler qui permet de construire un ensemble invariant autour d'un système donné. Cette technique garantit que les solutions d'Euler approchées sont attirées par un cycle limite. Nous appliquons la méthode sur différents systèmes, y compris des systèmes chaotiques avec des attracteurs "étranges". De plus, nous montrons qu'une combinaison de basique d'un échantillonnage aléatoire avec une méthode de calcul symbolique aide à traiter des problèmes de contrôle robuste pour les systèmes non linéaires. De plus, nous illustrons une condition de base garantissant qu'un système avec perturbation est robuste sous une séquence de contrôle répétée obtenue en résolvant un problème de contrôle optimal d'horizon. Enfin, nous avons unifié les principales contributions de la deuxième partie dans un outil appelé ORBITADOR qui vérifie la stabilité d'un système donné et retourne notamment des graphiques contenant l'évolution du système dans différentes vues et la forme de l'invariant s'il existe
Origine : Version validée par le jury (STAR)