Boolean-logic driven Markov processes (BDMPs) is a prominent dynamic extension of static fault trees to model repairable and complex dynamic systems. While BDMPs are intensively used in an industrial context for dependability analysis of energy systems, its formal semantics has not been systematically treated. To date, BDMPs are defined as a library of the domain-specific dependability-modelling language Figaro, a library that is neither open source nor publicly available. A rigorous semantic underpinning of BDMPs is indispensable for (1) developing BDMP analysis tools and (2) comparing its expressive power to other related reliability modelling languages. This paper presents a formal semantics to BDMPs using Markov automata (MA), an extension of continuous-time Markov chains (CTMCs) with action transitions that can be used to compose complex MA from smaller MA. This enables us to provide a compositional semantics. That is, we express the semantics of each individual BDMP element as an MA and obtain the MA for the entire BDMP by combining the MA of its elements. This makes the semantics comprehensible, for those who are familiar with automata theory, and easily extensible with new BDMP elements, e.g., to model security aspects. After the entire BDMP is considered, the actions in its MA that were used to “glue” the MA of BDMP elements, are ignored. This results in a CTMC that is amenable to exact numerical analysis by, e.g., efficient probabilistic model-checking techniques. We report on a prototypical implementation of our semantics and empirically show that our semantics yields dependability metrics that correspond to the interpretation by the Figaro knowledge base of BDMPs.

This paper presents a probabilistic model-checking tool for FIGARO, a multi-formalism modelling language that includes e.g., generalised stochastic Petri nets, Boolean-logic driven Markov processes, telecommunication networks, dynamic reliability block diagrams, process diagrams, and electric circuits. FIGARO has been developed and maintained by EDF for the analysis of system dependability such as reliability, availability and maintainability. We present a probabilistic model-checking tool for FIGARO models. It combines efficient, fully automated verification algorithms with numerical analysis techniques. Whereas the existing FIGARO tools, the Monte Carlo simulator YAMS and the most-probable-sequence explorer FiGSEQ, provide respectively statistical guarantees and upper bounds for unreliability and unavailability, our tool provides hard guarantees: its results are correct up to a given numerical accuracy. The key ingredient is the tool-component FiGAROAPI that enables the state-space generation for FIGARO models thus facilitating model checking. This paper describes the details of FiGAROAPI and empirically evaluates the feasibility and merits of the proposed framework. FiGAROAPI leverages upon the state-of-the-art STORM model checker as back-end, and it can model check various types of formalism in their FIGARO representation.

Adding repairs to dynamic fault trees (DFTs) is intricate and has given rise to several different, unfortunately inconsistent, interpretations. This is mainly due to many possible repair behaviours for each dynamic gate. This paper takes a pragmatic perspective and considers repair behaviours that have shown to be of long-standing industrial use in another, related, reliability formalism: Boolean logic-driven Markov processes (BDMPs). BDMPs are intensively used by the largest electrical energy producer and distributor in France to model and assess the reliability of repairable energy systems of different kinds. This paper takes the repair mechanisms of BDMPs as starting point and lifts them to repairable DFTs (rDFTs) by providing a set of BDMP-to-rDFT translation rules. The result is a repairable variant of DFTs in which repairs are interpreted consistently with BDMPs, in which repairs are a key asset. We empirically validate the correctness of this transformation by assessing the availability of a multiprocessor computing system and comparing the probabilistic model checking results of the obtained rDFTs against those for the original BDMPs.

Static Fault Trees (SFTs) are a key model in reliability and safety analysis. Various extensions have been developed to model, e.g., functional dependencies, state-dependent failures, and SPARE elements. This paper studies the expressive power of two important extensions of SFTs: Dynamic Fault Trees (DFTs) and Boolean Logic Driven Markov Processes (BDMPs). We outline a set of BDMP-to-DFT translation rules and apply them to thirty-three BDMP test cases modeling various scenarios of security, software and system reliability. The main contribution is a DFT modeling an industrial BDMP benchmark study of a Nuclear Power Plant (NPP). Although this DFT does not consider repairs, it is one of the largest industrial cases reported so far and is challenging for DFT analysis. We compare the performance and capabilities of analysis tools for BDMPs-the Monte-Carlo simulation tool YAMS, the proprietary Markovian analysis tool FigSeq-and the DFT analysis capability of the probabilistic model checker Storm. We also address how to do a system sensitivity analysis of the NPP benchmark using probabilistic model checking.