OFFIS and Carl von Ossietzky University (Oldenburg, Germany)
Interactive Markov Chains
CADP (Construction and Analysis of Distributed Processes)
Today's transportation systems become ever more complex and rely to
a large extent on embedded systems. Typically such systems come
equipped with sophisticated redundancy and monitoring concepts to
achieve a high degree of fault-tolerance. Fault injection, i.e.,
the injection of particular failure behaviour into the nominal
behaviour of a formal system model, has been proven to be a suitable
method to investigate the effectiveness of these fault-tolerance
recipes. Based on such an extended system model, the ISAAC project
developed methods and tools to automatically compute fault trees and
extract Minimal Cut Sets (MCSs). Intuitively, an MCS describes a
minimal combination of faults that can cause a safety critical
situation to occur. However, in practice such qualitative analyses
are not sufficient and quantitative safety assessment, taking concrete
fault occurrence rates (e.g., taken from technical specification) into
account, becomes imperative.
Taking into account all faults, the probability of reaching a safety critical state is analysed based on a Statecharts model extended by fault injection and annotated with fault occurrence distributions. The labeled transition system (LTS) model underlying the extended Statecharts description is generated and minimized modulo branching bisimulation. Then, stochastic time constraints, given as continuous time Markov chains (CTMCs), are incorporated into the LTS, in order to delay firing of particular (failure) transitions. The stochastic process algebra of Interactive Markov Chains (IMCs) makes it possible to handle the orthogonal combination of LTSs and CTMCs. A newly devised path encoding allows for the computation of MCS specific LTS variants, retaining the contribution of the faults in a particular minimal cut set, while disregarding contributions of other faults. This process finally yields a uniform continuous time Markov decision process (uCTMDP), on which the worst-case probability to reach a safety critical state within a given time bound is computed using timed reachability analysis.
This analysis approach is illustrated on a train odometer controller system, which consists of two independent sensors used to measure speed and position of a train, and a monitoring component in charge of continuously checking the status of both sensors. The minimization modulo branching bisimulation is carried out using symbolic algorithms, the minimization modulo stochastic branching bisimulation is performed using CADP, and the timed reachability analysis is done using the MRMC model checker. The additional complexity introduced in the model by the incorporation of stochastic time constraints is compensated by the stochastic branching bisimulation reduction.
The approach proposed enables the system developers to focus their
work on those parts of the systems where improvements will yield most
impact. Due to the preservation of the actual sequences of faults by
the MCSs, the derived measures are more accurate than conventional
naive or manual safety assessment techniques. Thanks to automation,
these measures can be derived without any extra effort directly from
the design model. Furthermore, by incorporating stochastic non failure
behaviour (e.g., repair rates of transient faults) into the modelling
and cut set analyses, again the accuracy can be improved, that is, a
less pessimistic assessment is derived.
Eckard Bode, Thomas Peikenkamp, Jan Rakow, and Samuel Wischmeyer.
"Model Based Importance Analysis for Minimal Cut Sets". Proceedings of
the 6th International Symposium on Automated Technology for Verification
and Analysis (Seoul, Korea), pp.303-317, LNCS Vol. 5311, October 2008.
Available on-line at: http://www.springerlink.com/content/h7lt157707t47h56/
or from the CADP Web site in PDF or PostScript
Safety Analysis & Verification Group
Tel: +49 441 9722-525
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies