Research

Formal models for safety-security decisions in cyber-physical systems.

Case studies across satellites, smart grids, research reactors, flexible production lines, and autonomous-systems collaborations. The work also extends into game-theoretic attacker-defender analysis through supervised thesis topics on PRISM, MDP translations, game automata, and quantitative trade-offs.

Safety-security co-analysisAttack-defense treesAttack-fault-defense treesStatistical model checkingCyber-physical systems

View publications Discuss collaboration

Research focus

Safety, security, and formal methods for cyber-physical systems.

Safety: fault trees, reliability, dependability

Security: attack-defense trees, threats, countermeasures

Formal methods: model checking, SMC, MDPs, game theory

Safety

Fault Trees

Security

ADTs

Formal Methods

SMC · PRISM

Co-analysis

Dependability

Game Theory

CPS risk evidence

AFDTs · SMC · MDPs · strategies

Method flow

Model, verify, quantify, decide.

The core research pattern is to turn domain risk into analyzable structure, then use formal evidence to support practical engineering choices.

Model

Attack, fault, defense structure

Verify

SMC and formal properties

Quantify

Cut sets, probabilities, trade-offs

Decide

Evidence for engineering action

Case studies

Research domains and outcomes.

Each case study is structured around the problem, domain context, method, tools, result, publication link, and why the work matters.

2024 · SAFECOMP / 2025 preprintPhD Researcher, University of Twente

Satellite Safety-Security via Attack-Fault-Defense Trees

Safety-security risk mitigation for satellite missions with attack-fault-defense trees.

Problem: Satellite ground-segment risks combine accidental failures, malicious attacks, and defenses that interact rather than stay in separate safety/security silos.

Method: Applied attack-fault-defense trees to model attacks, component failures, defenses, inhibition relations, and qualitative mitigation paths.

Outcomes

Formalized attack-fault-defense tree semantics with safety and security cut sets
Quantified dependencies for satellite missions and grid protection scenarios
Published at SAFECOMP 2024 with follow-up arXiv preprint (2504.00988)

Attack-Fault-Defense TreesCut-set reasoningMission risk analysisSafety-security co-analysis

Read case study arXiv 2504.00988

22 Jun - 20 Jul 2024Visiting Researcher, National University of Rio Cuarto

Optimal Spare Management for Research Reactors

Statistical model checking for spare-part strategies with INVAP SE.

Problem: Spare-part planning for research reactors must balance reliability targets, limited inventory, maintenance decisions, and stochastic failure behavior.

Method: Modeled maintenance and spare policies with statistical model checking to compare candidate strategies under uncertainty.

Outcomes

Modeled maintenance and spare policies for research reactors with stochastic behaviors
Explored optimal strategies via statistical model checking to meet reliability targets
Joint work with INVAP SE published in STTT 2025

UPPAAL SMCStatistical model checkingReliability modelingIndustrial case study

Read case study STTT 2025

2024 · ISGT EuropePhD Researcher, University of Twente

Safety and Security Dependencies for GridShield

Modeled safety-security dependencies for smart-grid protection and operational resilience.

Problem: Modern electrical grids expose coupled safety and security dependencies across cyber components, physical processes, and operational controls.

Method: Identified dependency structures between safety hazards, security threats, and grid-protection decisions.

Outcomes

Mapped safety and security dependencies for grid-protection scenarios
Connected formal risk modeling with energy-domain concerns and requirements
Published at IEEE ISGT Europe 2024

Dependency modelingSafety-security co-analysisSmart-grid risk analysis

Read case study ISGT Europe 2024

2021Researcher, University of Southern Denmark

Industry 4.0 Flexible Production Line Security

Modeled a flexible Industry 4.0 cyber-physical system to validate safety and security controls.

Problem: Flexible Industry 4.0 systems need to preserve operational adaptability while controlling risk from untrusted assets and variable workflows.

Method: Modeled CPS behavior and security controls with statistical model checking and strategy-oriented verification.

Outcomes

Modeled Industry 4.0 assets and communication paths for safety-security validation
Designed controls to reduce risk from untrusted assets while keeping flexibility
Connected to the 2021 FedCSIS and CoRR work on CPS verification and optimization

UPPAAL SMC/StrategoCyber-physical systemsRisk assessmentModel checking

Read case study FedCSIS 2021

Toolchain

From formal model to decision evidence.

Methods and tools that connect formal models with measurable engineering evidence.

UPPAAL SMC

PRISM

CPN Tools

Statistical Model Checking

Research network

Collaboration across Europe, South America, and East Asia.

Work anchored at the University of Twente, with a Project MISSION secondment in Rio Cuarto and two dated research stays at the Institute of Software in Beijing.

Netherlands

University of Twente

Argentina

Rio Cuarto, 22 Jun - 20 Jul 2024

China

Beijing, 8 Apr - 7 May 2025 and 24 Feb - 16 Mar 2026

Selected work

Featured research threads.

Satellite Safety-Security via Attack-Fault-Defense Trees; Optimal Spare Management for Research Reactors; Safety and Security Dependencies for GridShield.

Start a research conversation