Inria Grenoble - Rhône-Alpes and LIG, Grenoble (FRANCE)
CNRS/VERIMAG, Grenoble (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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,
Available on-line at: https://hal.inria.fr/hal-03348046/en
or from the CADP Web site in PDF or PostScript
Inria Grenoble - Rhône-Alpes
655, avenue de l'Europe
38330 Montbonnot Saint Martin
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|