Description

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

References

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