Maison Jean Kuntzmann
28 avril 2014 - 13h00
Vérification et synthèse quantitative (Phd Defense)
par Christian VON ESSEN de Verimag/UJF
28 avril 2014 - 13h00
Vérification et synthèse quantitative (Phd Defense)
par Christian VON ESSEN de Verimag/UJF
Résumé : Cette thèse contribue à l'étude théorique et a l'application de la vérification et de la synthèse quantitative. Nous étudions les stratégies qui optimisent la fraction de deux récompenses des MDPs. L'objectif est la synthèse de régulateurs efficaces dans des environnements probabilistes. Premièrement nous montrons que les stratégies déterministes et sans mémoire sont suffisants. Sur la base de ces résultats, nous proposons trois algorithmes pour traiter des modèles explicitement encodées. Notre évaluation de ces algorithmes montre que l'un de ces derniers est plus rapide que les autres. Par la suite nous proposons et mettons en place une variante symbolique basé sur les diagrammes de décision binaire. Deuxièmement, nous étudions le problème de réparation des programmes d'un point de vue quantitatif. Celà conduit à une reformulation de la réparation d'un log: que seules les exécutions fautives du programme soient modifiées. Nous étudions les limites de cette approche et montrons comment nous pouvons assouplir cette nouvelle exigence. Nous concevons et mettons en œuvre un algorithme pour trouver automatiquement des réparations, et montrons qu'il améliore les modifications apportées aux programmes. Troisièmement, nous étudions une nouvelle approche au framework pour la vérification et synthese quantitative. La vérification et la synthèse fonctionnent en tandem pour analyser la qualité d'un contrôleur en ce qui concerne, par exemple , de robustesse contre des erreurs de modélisation. Nous considèrons également la possibilité d'approximer la courbure de Pareto, qui appataît de la combinaison du modèle avec de multiples récompenses. Cela nous permet à la fois d'étudier les compromis inhérents au système et de choisir une configuration adequate. Nous appliquons notre framework aux plusieurs études de cas. La majorité de l'étude de cas est concernée par un système anticollision embarqué (ACAS X). Nous utilisons notre framework pour aider à analyser l'espace de conception du système et de valider le controleur en cours d'investigation par la FAA. En particulier, nous contribuons l'analyse par PCTL et stochastic model checking.
Jury :
Marta KWIATKOWSKA - Prof University of Oxford - Rapporteur
Jean-François RASKIN - Prof Université Libre de Bruxelles - Rapporteur
Alain GIRAULT - Dr Inria Rhône-Alpes - Examinateur
Ahmed BOUAJJANI - Prof Université Paris Diderot - Examinateur
Saddek BENSALEM - Pr. UJF - Directeur de thèse
Barbara JOBSTMANN -Dr CNRS/EPFL - CoDirecteur de thèse
