1. Explaining Safety Violations in Real-Time Systems
- Author
-
Thomas Mari, Thao Dang, Gregor Gössler, Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS), This work has been partially supported by the projects Univ. Grenoble Alpes IRS SEC, ANR DCore (ANR-18-CE25-0007), and ANR-CREST-JST CyphAI., ANR-18-CE25-0007,DCore,Debogage causal pour systèmes concurrents(2018), ANR-20-JSTM-0001,CyphAI,Méthodes formelles pour l'analysis et le développement de systèmes cyber-physiques intégrant l'intelligence artificielle(2020), INRIA, and Verimag, Université Grenoble Alpes
- Subjects
safety ,Safety property ,[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] ,Computer science ,causal explanations ,0202 electrical engineering, electronic engineering, information engineering ,real-time ,020207 software engineering ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,Hardware_PERFORMANCEANDRELIABILITY ,02 engineering and technology ,Fault (power engineering) ,Reliability engineering - Abstract
International audience; We tackle the problem of explaining faults in real-time systems. Intuitively, an explanation of the violation of a safety property by an execution is a concise excerpt of the faulty execution that retains only the elements that were relevant for entailing the violation, thus exhibiting how causes accumulate over time and propagate to entail the effect. Fault explanation therefore goes beyond the well-known concepts of fault diagnosis and localization.We provide a formal definition of causal explanations on dense-time models, based on the well-studied formalisms of timed automata and zone-based abstractions. Our approach is able to account for limited observability of the faulty execution. We propose a symbolic formalization to effectively construct such explanations, which we have implemented in a prototype tool. We illustrate our approach on several examples.
- Published
- 2021
- Full Text
- View/download PDF