Model Based Importance Analysis for Minimal Cut Sets

Organisation:	OFFIS and Carl von Ossietzky University (Oldenburg, Germany)
Method:	Statecharts Interactive Markov Chains
Tools used:	STATEMATE CADP (Construction and Analysis of Distributed Processes) MRMC
Domain:	Transport Safety.
Period:	2008
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Bode-Peikenkamp-Rakow-Wischmeyer-08] 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
Contact:	Thomas Peikenkamp Safety Analysis & Verification Group OFFIS e.V. Escherweg 2 26121 Oldenburg Germany Tel: +49 441 9722-525 Email: Thomas.Peikenkamp@offis.de
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page