Joost Pieter Katoen

Title: “Automated Analysis and Synthesis of Fault Trees”


Fault trees are pivotal in safety and reliability engineering. They are applied at industrial scale, and have been subject to standards in many application areas. Modern fault-tree dialects can model redundancies, functional dependencies, repairs, spare elements, activation mechanisms, and so forth. Their analysis is however a serious bottleneck: analysis techniques do not scale and require manual effort.

I will show how techniques from formal verification can be used to:

  • ¬†simplify fault trees prior to their expensive analysis, b. analyse measures that go beyond reliability and availability, and c. enable fault tree analysis of gigantic fault trees.

I explain the key algorithmic principles and showcase its improvement on some industrial cases: the safety for autonomous vehicle guidance, and the reliability of railway station areas. I finally argue how recent developments in the automated synthesis of probabilistic models pave the way towards algorithmic fault tree generation.


Joost-Pieter Katoen is a Distinguished Professor with RWTH Aachen University, Germany, and is part-time professor at the University of Twente, The Netherlands. He received a honorary doctorate degree from Aalborg University, Denmark in 2017. His research interests include formal methods, model checking, concurrency theory, safety analysis and reliability, and probabilistic computation. He coauthored more than 75 journal papers, 200 conference papers, and the book “Principles of Model Checking”. He chaired the steering committee of ETAPS (2014-2019), the largest European conference on software, and is steering committee member of CONCUR, QEST, and FORMATS. He is an elected member of Academia Europaea (since 2013), and holder of an ERC Advanced Research Grant on probabilistic programming (2017).