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.

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.

Attack modeling has recently been adopted by security analysts as a useful tool in risk assessment of cyber-physical systems. We propose in this paper to model the Stuxnet attack with BDMP (Boolean logic Driven Markov Processes) formalism and to show the advantages of such modeling. After a description of the architecture targeted by Stuxnet, we explain the steps of the attack and model them formally with a BDMP. Based on estimated values of the success probabilities and rates of the elementary attack steps, we give a quantification of the main possible sequences leading to the physical destruction of the targeted industrial facility. This example completes a series of papers on BDMP applied to security by modeling a real case study. It highlights the advantages of BDMP compared to attack trees often used in security assessment.

Safety and security issues are increasingly converging on the same critical systems, leading to new situations in which these closely interdependent notions should now be considered together. Indeed, the related requirements, technical and organizational measures can have various interactions and side-effects ranging from mutual reinforcements to complete antagonisms. A better characterization of these interdependencies is needed to ensure a controlled level of risk for the systems concerned by such a convergence. This paper describes the state of the art on this open issue and presents a new approach based on BDMP (Boolean logic Driven Markov Processes), allowing graphical modeling and advanced characterization of safety and security interdependencies. A simple use-case is used through diverse modeling variants, illustrating the capabilities, the contributions but also the limits with respect to other works dealing with safety and security interdependencies. We believe the proposed approach constitutes an original and valuable tool which could find its place in the ongoing research aiming at tackling this open and challenging task.