学术文献库

A Boolean logic driven Markov process (BDMP) is a dependability analysis model that defines a continuous-time Markov chain (CTMC). This formalism has high expressive power, yet it remains readable because its graphical representation stays close to standard fault trees. The size of a BDMP is roughly speaking proportional to the size of the system it models, whereas the size of the CTMC specified by this BDMP suffers from exponential growth. Thus quantifying large BDMPs can be a challenging task. The most general method to quantify them is Monte Carlo simulation, but this may be intractable for highly reliable systems. On the other hand, some subcategories of BDMPs can be processed with much more efficient methods. For example, BDMPs without repairs can be translated into dynamic fault trees, a formalism accepted as an input of the STORM model checker, that performs numerical calculations on sparse matrices, or they can be processed with the tool FIGSEQ that explores paths going to a failure state and calculates their probabilities. BDMPs with repairs can be quantified by FIGSEQ (BDMPs capturing quickly and completely repairable behaviors are solved by a different algorithm), and by the I&AB (Initiator and All Barriers) method, recently published and implemented in a prototype version of RISKSPECTRUM PSA. This tool, based exclusively on Boolean representations looks for and quantifies minimal cut sets of the system, i.e., minimal combinations of component failures that induce the loss of the system. This allows a quick quantification of large models with repairable components, standby redundancies and some other types of dependencies between omponents. All these quantification methods have been tried on a benchmark whose definition was published at the MARS 2017 workshop: the model of emergency power supplies of a nuclear power plant. In this paper, after a recall of the theoretical principles of the various quantification methods, we compare their performances on that benchmark.