author: Joshua de Bie
title: How safe is your system?
keywords: probabilistic timed automata, dynamic fault trees, case study, model checking
topics: Case studies and Applications
committee: Arnaud van Harmelen ,
Carlos Esteban Budde ,
Mariƫlle Stoelinga
started: November 2017
end: February 2018


RAMS (Reliability, Availability, Maintenance, Safety) requirements are utmost important for safety-critical systems like nuclear power plans, power grids, and railroad infrastructure, and often imposed by law. A widely applied standard for RAMS analysis is the use of fault tree analysys (FTA). There are a lot of different approaches to deal with FTA, where a very prominent one is to use continuous timed Markov chains (CTMCs). 

However, the expresivness of this method is limited by several factors, like the state space explosion problem. Therefore, we want to look into another model, namely probabilistic timed automata (PTA) and compare those to existing methods.

Your tasks will include:

  • study of existing FTA methods
  • study of PTAs and their model checking
  • modelling fault trees using PTAs
  • conducting several case studies and compare the results


  1. Model Checking for Probabilistic Timed Automata. (Digital version available here)
  2. Dynamic Fault Tree analysis using Input/Output Interactive Markov Chains. (Digital version available here)

Additional Resources

  1. Paper