Maison Jean Kuntzmann
28 April 2014 - 13h00
Quantitative verification and synthesis (Phd Defense)
by Christian VON ESSEN from Verimag/UJF
28 April 2014 - 13h00
Quantitative verification and synthesis (Phd Defense)
by Christian VON ESSEN from Verimag/UJF
Abstract: This thesis contributes to the theoretical study and application of quantitative verification and synthesis. We first study strategies that optimize the ratio of two rewards in MDPs. The goal is the synthesis of efficient controllers in probabilistic environments. We prove that deterministic and memoryless strategies are sufficient. Based on these results we suggest 3 algorithms to treat explicitly encoded models. Our evaluation of these algorithms shows that one of these is clearly faster than the others. To extend its scope, we propose and implement a symbolic variant based on binary decision diagrams, and show that it cope with millions of states. Second, we study the problem of program repair from a quantitative perspective. This leads to a reformulation of program repair with the requirement that only faulty runs of the program be changed. We study the limitations of this approach and show how we can relax the new requirement. We devise and implement an algorithm to automatically find repairs, and show that it improves the changes made to programs. Third, we study a novel approach to a quantitative verification and synthesis framework. In this, verification and synthesis work in tandem to analyze the quality of a controller with respect to, e.g., robustness against modeling errors. We also include the possibility to approximate the Pareto curve that emerges from combining the model with multiple rewards. This allows us to both study the trade-offs inherent in the system and choose a configuration to our liking. We apply our framework to several case studies. The major case study is concerned with the currently proposed next generation airborne collision avoidance system (ACAS X). We use our framework to help analyze the design space of the system and to validate the controller as currently under investigation by the FAA. In particular, we contribute analysis via PCTL and stochastic model checking to add to the confidence in the controller.
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
