Explaining Safety Violations in Real-Time Systems

Organisation:	Inria Grenoble - Rhône-Alpes and LIG, Grenoble (FRANCE) CNRS/VERIMAG, Grenoble (FRANCE)
Functionality:	Embedded Systems
Tools used:	Kronos Minim CADP (Construction and Analysis of Distributed Processes)
Period:	2021
Description:	Embedded real-time systems already became ubiquitous and the number of such devices is growing exponentially. There is a rich body of work on software engineering, formal verification, and certification of such systems. A complementary design approach is accountability, which aims at building systems such that the responsibilities for a failure can be identified and explained after the failure occurred. An explanation is a concise excerpt of the observed execution that retains only the elements entailing the violation. The construction of explanations is a challenging task that requires, on the one hand, to convey the right amount of information for understanding the causes of the violation, and to comply with the nature of embedded systems (infinite state spaces and limited observability of states and events). This work contributes to the construction of explainable embedded real-time systems by investigating how to construct, from a system model, a safety property, and an execution log that violates the property, a concise explanation of how the log brought about the violation of the property. Firstly, a formal definition of causal explanations on dense-time models is proposed, based on timed automata. Secondly, a symbolic approach is proposed to effectively construct explanations. The approach has been implemented in a prototype tool relying on Kronos for the composition of timed automata, Minim for the generation of the quotient graph, and the BCG_MIN tool of CADP for bisimulation reductions. The tool was successfully applied to a dual-chamber implantable pacemaker model.
Conclusions:	This work proposed a novel approach to explain the violation of a safety property by a real-time system. Basically, an explanation is formed by the parts of the behaviors that are consistent with the log, that jointly contributed to move the system into the failure state. Future work includes establishing formal properties of explanations, constructing explanations online, and extending the analysis to more general classes of hybrid systems.
Publications:	[Mari-Dang-Goessler-21] Thomas Mari, Thao Dang, and Gregor Goessler. "Explaining Safety Violations in Real-Time Systems". Proc. of the 19th International Conference on the Formal Modeling and Analysis of Timed Systems (FORMATS'2021), Paris, France, LNCS vol. 12860, pp. 100-116. Springer Verlag, 2021. Extended version available as Inria Research Report RR 9420, September 2021. Available on-line at: https://hal.inria.fr/hal-03348046/en or from the CADP Web site in PDF or PostScript
Contact:	Gregor Goessler Inria Grenoble - Rhône-Alpes 655, avenue de l'Europe 38330 Montbonnot Saint Martin FRANCE Email: gregor.goessler@inria.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page