Explaining Boolean-Logic Driven Markov Processes using GSPNs

European Dependable Computing Conference, vol. 10877, pp. 119–126

Abstract

Boolean-logic driven Markov processes (BDMPs) is a graphical language for reliability analysis of dynamic repairable systems. BDMPs are capable of defining complex interdependencies among failure modes such as functional dependencies and state-dependent failures. The interpretation of BDMPs is non-trivial due to the many possible complex interactions of activation and failure mechanisms. This paper presents a formal semantics of repairable BDMPs by using generalized stochastic Petri nets (GSPNs). Our semantics is modular and thus easily extendable to other elements, e.g., leaves dedicated to security applications. Priorities on GSPN transitions are used to impose a partial order on various possible interleaving of activation and failure mechanisms. The semantics is realized by the prototypical tool BDMP2GSPN that converts a Figaro description of a BDMP into a GSPN. The reliability and availability metrics of BDMPs are obtained using the probabilistic model-checking capability of the existing GreatSPN tool. Experiments show that our GSPN semantics corresponds to the BDMP interpretation by the tool yet another Monte Carlo simulator (YAMS).

Authors 3

1. Shahid Ali Khan Aachen Software Modeling and Verification

   RWTH Aachen University

   Affiliation as printed

   Software Modeling and Verification, RWTH Aachen University, Aachen, Germany

2. Joost-Pieter Katoen Aachen Software Modeling and Verification

   RWTH Aachen University

   Affiliation as printed

   Software Modeling and Verification, RWTH Aachen University, Aachen, Germany

3. Marc Bouissou

   Électricité de France (France)

   Affiliation as printed

   EDF-R&D, Electricité de France, Palaiseau, France