title: A Compositional Framework for Dynamic Reliability Block Diagrams
topics: Dependability, security and performance
committee: Mariƫlle Stoelinga


Reliability Block Diagrams (RBDs) are a graphical language to model and analyze the reliability of software and hardware systems. They model the failure of a system in terms of the failure of its component. Dynamic Reliability Block Diagrams (DRBDs) extend RBDs with dynamic behaviour.

In this project, we want to improve the analysis for DRBDs by translating them to Input/Output Markov Chains (IOIMC). This translation should be compositional, i.e. we attach a small IOIMC to each block in the DRBDs. Then, we can analyze the IOIMC model with the CADP model checker.

Previously, we have made a translation of Dynamic Fault Trees to IOIMCs and we achieved great state space reductions (e.g 1,300 instead of 32,000 states) and now we want to apply a similar mechanism to a the DRBD formalism.


  • Understand the DRBD formalism
  • Translate each DRBD-component to a IOIMC model
  • Implement this translation in a tool
  • Perform experiments


  • Familiarity with state-transition formalisms
  • Programming experience
  • Experience with the use of model checkers (UPPAAL, CADP, SPIN, ...)