Contributions aux méthodes formelles pour les systèmes temporisés et probabilistes / Contributions on Formal Methods for Timed and Probabilistic Systems

Soutenance d’HDR d’Ocan Sankur, équipe SUMO, le 2 octobre 2023 à 14h en salle Métivier / Ocan Sankur’s HDR defense, SUMO team – 2023, October 2nd, 2pm, Metivier room

Contributions aux méthodes formelles pour les systèmes temporisés et probabilistes

Les méthodes formelles sont un terme générique désignant des techniques rigoureuses de spécification et de vérification des systèmes informatiques, ou de construction de ces systèmes avec des garanties mathématiques sur leur exactitude ou sur l'absence de bugs. Le model checking est un ensemble de techniques permettant de prouver formellement les propriétés d'un modèle donné, tandis que la synthèse de contrôleur consiste,
à l'aide de techniques similaires, à compléter la description d'un système ouvert pour garantir une propriété donnée par construction.
L'une des cibles des méthodes formelles sont les systèmes présentant des aspects quantitatifs tels que les contraintes temps réel et les probabilités.
Dans cette thèse, je résume mes contributions sur des algorithmes de model checking et de synthèse de contrôleur pour des systèmes temporisés et probabilistes,
en particulier, pour les formalismes des automates temporisés et des processus de décision de Markov.

Contributions on Formal Methods for Timed and Probabilistic Systems

Formal methods is an umbrella term for rigorous techniques for specifying and verifying computer systems, or building
such systems with mathematical guarantees on their correctness, or on the absence of bugs of a given kind.
Model checking is a set of techniques that can formally prove properties of a given model; while controller synthesis consists,
using similar techniques, in completing the decription of an open system to ensure a given property by construction.
One of the targets of formal methods is systems with quantitative aspects such as real-time constraints and probabilities.
In this thesis I summarize my contributions on algorithms for model checking and controller synthesis on timed and probabilistic systems,
focusing on timed automaton and Markov decision process formalisms.