Formal methods for risk analysis

Would it not be great to live in a world where computers never crash, trains always ride and banks are never hacked?

This is the ultimate goal of risk management. In FMT, we work on the risk analysis phase, where one identifies, evaluates and prioritizes risks, to come up with (cost-)effective countermeasures. By using mathematical models, we can not only reason about risk, but quantify risk as well. As risk models from industry become very large very quickly, creating algorithms that analyze risk models efficiently is an important area of research.

Prominent mathematical models include graph models such as fault trees (for safety), attack trees (for security), binary decision diagrams, and Bayesian networks. Application areas we have considered so far include cybersecurity, medical devices, and robotics, but we are interested in many applications: if you have one of your own, please come to us.

Projects for Formal methods for risk analysis roughly fall within some or more of the following categories:

If you have an idea related to any of these, please contact us directly. Alternatively, you can work on one of the concrete proposals below.

Some of the research in Formal methods for risk analysis is closely related to that of quantitative analysis, as it relies on stochastic model-checking techniques. Conversely, many examples and case studies for quantitative analysis come from risk management.

  • Attack tree metrics

    Supervisor: Milan Lopuhaä-Zwakenberg and Reza Soltani

    Attack trees are a popular and useful tool to model a system's vulnerability to attackers. They are used in quantitative security analysis: they can be used to calculate security metrics such as the minimal time or resources an attacker needs to successfully compromise the system. As attack trees can grow quite large in practice, there is an ongoing need for algorithms that can calculate security metrics on a feasible timescale.

    In this project, the student adds to this field of research by implementing proposed algorithms, inventing new ones, or analyzing the behaviour of existing methods. Some possible avenues for research are:

    • Linear programming: many security metrics can be phrased as optimization problems (such as the minimal cost of a succesful attack). Therefore, a student could create new metric calculation algorithms based on optimization techniques such as linear programming.
    • Multi-metric analysis: it often makes sense to consider the interplay between metrics: one attack may be more costly to the attacker than another, but do more damage in return. There are some ideas on how to co-analyze metrics, but these have hardly been implemented, and there is also plenty of room for new ideas.
    • Attack tree properties: As the problem of calculating security metrics is NP-hard, many existing algorithms are of worst-case exponential complexity. However, it is unclear how these algorithms fare in practice, and what properties of the attack tree have an impact on algorithm complexity.
    • Modular analysis: An underused idea in attack tree analysis is to split up the attack tree into so-called modules and analyze each module separately. This idea can be applied to many different algorithms, and it would be interesting to see what difference this makes on both a theoretical and an experimental level.

    Of course, there are many other possibilities, and students are welcome to bring their own ideas to the table.

  • Converting AFT to game automata

    Supervisor: Reza SoltaniMilan Lopuhaä-Zwakenberg

    In the cyber-physical domain, safety and security have a complex relationship that entails trade-offs. Specifically, taking steps to improve safety may weaken security, and vice versa. Security and safety are frequently looked into separately in different studies.

    When it comes to safety, Fault Trees (FT) analysis is frequently used to identify potential problems, such as component failures that propagate throughout a system. From a security perspective, we use Attack Trees (AT) to understand how attackers might break things down into smaller steps and elements to achieve their goals.

    Attack-Fault Trees (AFT) are utilized for a thorough study that considers elements related to safety and security. AFTs have limitations; for example, it is not possible to fully show the effect of safety and security on each other. One of the solutions is to convert AFTs into game automata.

     In earlier work, we have modeled FTs as a 1.5-player game [1]. One could use an analogous approach to model an AFT as a 2-player game. Such a time-game automaton could then be subject to comprehensive quantitative safety-security analysis using model checkers.

     Some research questions:

    • If the attacker knows about the safety failures, how does this affect the cost and probability of the attack?
    • Can attacks increase safety failure?


    1.        Soltani, R., Volk, M., Diamonte, L., Lopuhaä-Zwakenberg, M., Stoelinga, M. (2023). Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors. In: Cimatti, A., Titolo, L. (eds) Formal Methods for Industrial Critical Systems. FMICS 2023. Lecture Notes in Computer Science, vol 14290. Springer, Cham.

    For more information, please contact or

  • Converting decision trees into fault trees

    Supervisors: Lisandro Jimenez Roa, Milan Lopuhaä-Zwakenberg

    Decision trees and fault trees are two models to represent the reliability of complex systems. While the information they contain is mathematically identical, the fact that the models are formed in different ways means that they are used by different people for different reasons. Therefore, it would be interesting to convert decision trees to fault trees, but contrary to the opposite direction this conversion has not been explored so far.

    In this project, the student will study and develop algorithms to convert decision trees into fault trees. While it is reasonably straightforward to come up with naïve algorithms, we are particularly interested in how those algorithms can be improved by decreasing their computation time and by outputting smaller fault trees.

  • Improving the inference of risk models

    Supervisors: Matthias Volk, Lisandro A. Jimenez-Roa, Marijn Peppelman

    Risk models such as fault trees (FTs) are formalisms typically used in reliability engineering, safety, and risk analysis. A known drawback of FTs is the time-consuming manual construction of these models, making them prone to human errors and incompleteness. Thanks to the ever-increasing availability of inspection and monitoring data, the development of algorithms that take care of this task in a data-driven manner are possible.

    In [1] this challenge was tackled using multi-objective evolutionary algorithms, yielding compact and reliable FT models. Building upon this work, several interesting research directions are possible.

    Possible research directions

    • Boolean circuit design: Circuit designs aims to find circuits with a minimal number of logical gates representing a given Boolean function. FT models can be encoded by Boolean formulas. A possible research direction is to find and apply existing algorithms from circuit design for FT inference.
    • Guiding the evolutionary algorithms: The current algorithm [1] takes a long time to converge when randomly applying genetic operators. One possible research direction is therefore to investigate to what extent knowledge about the models can be included to guide the genetic operators.
    • Noisy and incomplete data sets: Current approaches only consider noise-free and complete failure data sets, which is of course not representative of real applications. Thus, it is interesting to investigate how to effectively deal and account for noise and incompleteness in failure data sets when inferring FT models in a data-driven manner.


    [1] Jimenez-Roa, L. A., Heskes, T., Tinga, T., & Stoelinga, M. I. A. (2021). Automatic inference of fault tree models via multi-objective evolutionary algorithms. Preprint available online.


    Most research directions encompass a prototypical implementation. It is therefore advisable to be familiar with the Python programing language.

  • A long awaited marriage: investigating safety/security interactions in real-world scenarios

    Supervisors: Stefano Maria Nicoletti, Reza Soltani

    The introduction and adoption of new technologies implies the rise of new risks, related both to accidental damage (safety) and to malicious attacks (security). Furthermore, safety and security are often intertwined: passwords protect medical data from unauthorized access but are an obstacle for patients' safety during emergencies, IoT sensors can help to monitor the pressure levels of a pipeline but may provide extended attack surfaces for malicious hackers.
    The existence of interdependencies between safety and security calls for a better (formal) understanding of this kind of interactions:

    • At what level do safety and security interact? What interacts with what?
    • Do these interactions regard requirements, countermeasures, factors (etc.)?


    The suggested tasks are the following:

    • Together with your supervisor, decide on a case study of interest and investigate how safety and security interact in this setting. Case study scenarios can also be provided by your supervisor (e.g., a drone assembly factory).
    • Chose a formalism to analyse said case study (by discussing with your supervisors) and understand its modelling capabilities
    • Starting from the chosen case study, investigate which of the different interactions between safety and security are captured by the formalism of choice
    • Investigate at what level these interactions take place

    For this topic, you should have a strong interest in multidisciplinary research.

  • Improving the Common Vulnerability Scoring System (CVSS): Prioritizing Vulnerability Response

    Keywords: Vulnerability, CVE, CVSS, Vulnerability Scoring System, Security, Applied research

    Topics: Risk in High Tech Systems, Case Studies and Applications, Security

    Committee: Jeroen van der HamErnst Moritz Hahn, Stefano Maria Nicoletti 

    Project Description:

    The correct prioritization of actions to take after the discovery of new vulnerabilities is a key step in vulnerability management, analysis, handling and response. For many organizations this translates into using the Common Vulnerability Scoring System (CVSS) as a priority guide, paying particular attention to the technical severity of each vulnerability. Unfortunately, CVSS scores and their re-adaptations share a number of  issues that may undermine the choice of CVSS as the only parameter for actions prioritization: among these, it has been shown [1] that a high CVSS score does not always translate to publicly released exploits for that vulnerability or to high frequency of exploitation.

    To address this issue, [2] proposes a testable Stakeholder-Specific Vulnerability Categorization (SSVC) based on decision trees. The authors argue that decisions are a more useful output than severity as different organizations can make different decisions on how to react to vulnerabilities based on their different priorities.

    Although promising, this strategy leaves the door open to further refinement, mainly due to its preliminary nature. In particular, more testing is needed in order to assess decision trees' reliability, i.e., “reliable means that two analysts, given the same vulnerability description and decision process description, will reach the same decision.” In order for the decision trees to be reliable, the methodology proposed in [2] should be repeated with different groups, from diverse backgrounds and experiences.


    The topic will be developed alongside the student, however suggested tasks are the following:

    1. Understand the capabilities of decision trees and the SSVC
    2. Get in touch with different analyst groups with a chosen vulnerability description and decision process description
    3. Assess the reliability of the proposed framework
    4. Highlight possible shortcomings and suggest possible improvements


    Interest in cybersecurity, vulnerability management and problem solving.

    What will you gain?

    You will gain an understanding of the Common Vulnerability Scoring System (CVSS), its flaws and potential solutions to address them.

    Curious? Please, feel free to contact us for further discussion, even if you are still undecided.


    [1] Allodi, Luca and Fabio Massacci. A Preliminary Analysis of Vulnerability Scores for Attacks in Wild: The EKITS and SYM Datasets. BADGERS’12, Oct 5, 2012, Raleigh, North Carolina, USA.

    [2] Spring, Jonathan M., et al. Prioritizing Vulnerability Response: A Stakeholder Specific Vulnerability Categorization. Carnegie-Mellon University Pittsburgh, Pittsburgh United States, 2019.

  • Software fault trees

    Supervisor: Reza SoltaniStefano Nicoletti

    Fault trees are an important formalism to assess the reliability of systems. Typically, they model how failures propagate from component failures to system level failures, via gates like AND and OR.

    Fault trees have been very successfully applied to complex hardware systems, like railroads or chemical plants. However, software is getting more and more important. Hence, software fault trees have been developed to account for software failures as well.

    Research directions:

    The key idea of this project is to find out how Software fault trees work, and how they perform. Possible research directions are:

    • Developing methods to estimate the failure rates for software components.
    • Developing methods to automatically create fault trees for software, for example by a translation from specification languages such as UML.

    For more information, please contact or

  • Visualization of risks

    Supervisor: Mariëlle Stoelinga

    Fault trees are a popular model in risk analysis: they describe how failures propagate from components to system level: system components are modelled as leaves of the tree, and gates (like AND, OR, priority-AND) in a fault tree model how failures propagate to the top of the tree, which represents that the system has failed.
    A wide number of techniques is available to analyse fault trees, both in a qualitative and in a quantitative way: cut sets, BDDs, probabilistic analysis, etc.
    The goal of this project is to visualize the outcomes of such analyses: while standard GUIs exist to draw fault trees, and to add the information needed for the analysis, this is not true for the outcomes of the analysis: presentation of the results is usually done via simple plots. This can be done much better and nicer!
    Hence, we would like to develop more sophisticated and interactive means to visualize a fault tree: various visualization tools and frameworks can be deployed here --- making fault tree analysis a joy to look at.


    Your tasks will include:

    • study fault tree models
    • investigate state-of-the-art visualization tools
    • implement a fault tree visualizer
  • Condition assessment of sewer and water pipe networks using data-driven models

    SupervisorsLisandro Jimenez RoaMariëlle Stoelinga

    Assessing the condition of sewer and water pipe networks is vital for maintaining the reliability and safety of these essential infrastructure systems. Ageing and deteriorating pipes can cause various issues, such as leaks, breaks, and failures, leading to significant environmental and economic impacts. This project aims to investigate machine learning models for condition assessment in sewer and water pipe networks. These models will analyze historical inspection records to provide predictions of pipe conditions. Students will select and concentrate on one of the following research areas:

    1. Data Quality and Availability: This research area addresses the challenges arising from incomplete, inaccurate, and inconsistent data on sewer and water pipe conditions, which hinders the effectiveness of condition assessment and prediction models. The student will explore strategies for enhancing data quality and availability, such as data fusion techniques or crowdsourcing data. A tangible outcome will be a data quality improvement framework customized for the specific case study.
    2. Predicting Water Pipe Failure: This research area aims to develop more accurate models for predicting water main breaks to reduce service disruptions and enhance overall infrastructure management. Students will investigate machine learning or stochastic models for water pipe failure prediction, including random forests, decision trees, support vector machines, or Markov chain models. A tangible outcome will be a predictive model that can accurately forecast water pipe failures.
    3. Robust Sewer Pipe Deterioration Models: This research area focuses on constructing (or improving existing) models for predicting sewer pipe conditions by developing data-driven models to predict the type and severity of damage in sewer pipe networks. Emphasis will be placed on model validation and prediction uncertainty, contributing to more robust condition assessment and maintenance decision-making. Students will examine techniques such as Bayesian networks, Gaussian processes, ensemble learning, neural networks, decision trees, Markov chains, or regression models. Tangible outcomes will include an enhanced prediction model with quantified uncertainty estimates and a validated sewer pipe deterioration model that can predict damage types and severities with a measurable level of confidence.

    Case Study: The project will centre on a real-world case study focusing on either sewer or water networks. The case study will involve historical inspection data, including pipe covariates (material, geometry, location, etc.), damages, and severities. This practical approach will help validate the effectiveness of the developed models and ensure their applicability to real-world situations.

    Some literature of interest:

    • Hawari, Alaa, Firas Alkadour, Mohamed Elmasry, and Tarek Zayed. 2020. 'A state of the art review on condition assessment models developed for sewer pipelines', Engineering Applications of Artificial Intelligence, 93: 103721.
    • Laakso, Tuija, Teemu Kokkonen, Ilkka Mellin, and Riku Vahala. 2018. 'Sewer condition prediction and analysis of explanatory factors', Water, 10: 1239.
    • Nguyen, Lam Van, and Razak Seidu. 2022. 'Application of Regression-Based Machine Learning Algorithms in Sewer Condition Assessment for Ålesund City, Norway', Water, 14: 3993.
    • Sousa, Vitor, José P Matos, and Natércia Matias. 2014. 'Evaluation of artificial intelligence tool performance and uncertainty for predicting sewer structural condition', Automation in Construction, 44: 84-91.
    • Weeraddana, Dilusha, Bin Liang, Zhidong Li, Yang Wang, Fang Chen, Livia Bonazzi, Dean Phillips, and Nitin Saxena. 2020. 'Utilizing machine learning to prevent water main breaks by understanding pipeline failure drivers', arXiv preprint arXiv:2006.03385.
  • Design of web application for water and sewer management education

    SupervisorsLisandro Jimenez RoaMariëlle Stoelinga

    Water and sewer management plays an important role in maintaining public health, fostering environmental sustainability, and supporting economic growth. Due to global challenges such as climate change, urbanization, and population growth, the strain on water resources and infrastructure intensifies, leading to a rising need for proficient professionals. By developing a user-friendly, engaging, and accessible web application, this research aims to facilitate knowledge sharing and learning while endorsing best practices in water and sewer management. The research concentrates on identifying key design criteria, essential elements, and adopting a user-centric approach to establish a valuable educational resource that enhances efficiency and sustainability in water and sewer management practices.

    General Research Question: How can a web application be designed to effectively facilitate learning and knowledge sharing in the domain of water and sewer management?

    Students may choose one or more of the following research directions, depending on their interests and the project's scope:

    • Web Interface Design Criteria: This research direction aims to identify the key criteria for an effective web interface that promotes user engagement and learning in water and sewer management. Investigating best practices for web application design emphasizes usability, accessibility, responsiveness, and visual appeal. The expected outcome is a list of design principles and guidelines specific to water and sewer management education. Research Question: What are the key criteria for designing an effective web interface that promotes user engagement and learning in water and sewer management?
    • Essential Elements Identification: This direction seeks to determine the essential elements to include in the web application based on user needs and educational objectives. Researchers will analyze these factors to identify crucial elements such as interactive tutorials, case studies, quizzes, multimedia resources, a glossary, and/or a discussion forum. The expected outcome is a detailed description of these essential elements and their role in supporting learning and knowledge sharing. Research Question: What are the essential elements to include in the web application based on user needs and educational objectives in water and sewer management education?
    • Web Interface Design: This research direction focuses on designing an intuitive and visually appealing web interface that encourages user engagement and learning in water and sewer management. It involves creating wireframes and mockups for the web application that incorporates identified criteria and essential elements while ensuring an intuitive and visually appealing design. The expected outcome is a collection of wireframes and mockups ready for user feedback and refinement. Research Question: How can an intuitive and visually appealing web interface be designed to promote user engagement and learning in water and sewer management?
    • Prototype Development and Testing: In this direction, researchers will develop a functional prototype of the web application, incorporating the designed interface and essential elements while ensuring usability, responsiveness, and accessibility. The process includes implementing the designed web interface and essential elements into a functional prototype, testing its usability, responsiveness, and accessibility, and iterating based on feedback. The expected outcome is a functional prototype validated through usability testing and user feedback. Research Question: How can a functional prototype of the web application be developed and tested to ensure usability, responsiveness, and accessibility in water and sewer management education?