How safe is your system?

title:How safe is your system?
keywords:probabilistic timed automata, dynamic fault trees, case study, model checking
topics:Case studies and Applications
contact:dr. M.I.A. Stoelinga & D. Guck MSc & W. Ahmad MSc


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)