Maison du doctorat Jean Kuntzmann
17 November 2023 - 14h30
Causal explanations for reactive real-time systems (Phd Defense)
by Thomas Mari from VERIMAG (MOHYTOS), INRIA (SPADES)
Abstract: With the growing complexity of embedded systems, it is crucial to understand and localize sources of failures, for instance, to correct and improve the system.
In this thesis, we are interested in counterfactual analysis, more precisely the problem of computing causal explanations.
In order to do counterfactual analysis, one needs a model and to this end, we use discrete-time and dense-time models.
The first contribution of the thesis is a formal definition of causal explanations on discrete event systems, that we call choice explanations, constructed from a discrete function, that we call level of choice. We propose a symbolic approach to effectively construct such explanations. Furthermore, we illustrate our approach with several examples and a case study.
We also define a semantic function paired with a choice explanation. This semantic function returns the set of behaviors explained by a choice explanation. We identify a set of properties between an explanation and the observed failure and we prove the choice explanations satisfy those properties.
The second contribution is the extension of the definition of choice explanations to dense-time models, based on the well-studied formalism of timed automata and the strong time abstract bisimulation. The approach is also illustrated in several examples and a case study.
Regarding real-time systems, a major contribution of the thesis is a novel approach to construct causal explanations of failures from a quantitative function that we call robustness of choice or robustness for short. With our approach, there is no need to model the failures or faulty events, a semantic model and a safety specification are sufficient for explaining the failures. This robustness function assigns a value to every state of the system that reflects the ability of the system to avoid failure. We formalize a set of requirements for robustness functions in view of explaining the failures of a cyber-physical system. Some of these requirements are inspired by the properties of the discrete level of choice and are stronger in a dense-time model. The other additional requirements in a dense-time model allow to convey the concept of urgency in the explanation. Another important contribution is the definition of one instance of robustness function that can be computed for timed automata. With such an instance of robustness function, we can indeed compute causal explanations of the failures of real-time systems.
Thèse soutenue publiquement le 17 novembre 2023, devant le jury composé de :
GREGOR GOESSLER (Directeur de thèse)
DIRECTEUR DE RECHERCHE, INRIA CENTRE GRENOBLE-RHONE-ALPES
THAO DANG (Directrice de thèse)
DIRECTRICE DE RECHERCHE, CNRS DELEGATION ALPES
PATRICIA BOUYER-DECITRE (Examinatrice)
DIRECTRICE DE RECHERCHE, CNRS DELEGATION ILE-DE-FRANCE SUD
ERIC GAUSSIER (Examinateur)
PROFESSEUR DES UNIVERSITES, UNIVERSITE GRENOBLE ALPES
OLEG SOKOLSKY(Examinateur)
ASSOCIATE PROFESSOR, UNIVERSITY OF PENNSYLVANIA
STEPHAN LEUE (Rapporteur)
PROFESSEUR, UNIVERSITÄT KONSTANZ
DEJAN NICKOVIC (Rapporteur)
SENIOR SCIENTIST, AUSTRIAN INSTITUTE OF TECHNOLOGY
