Research
Overview
Artificial intelligence (AI) is increasingly used in cyber-physical systems (CPSs), which combine digital and physical components in applications ranging from medical devices and autonomous vehicles to humanoid assistant robots. As advanced AI makes these systems more complex, their behaviour becomes harder to analyze reliably. At the same time, their growing role in society exposes them to increasingly diverse and unpredictable operating conditions. It is therefore essential, yet challenging, to provide safety assurance: a clear argument, supported by reliable evidence, that a system meets its safety requirements, such as safe behaviour across operating conditions. Current assurance methods struggle to keep pace, with safety failures already have severe real-world consequences, such as fatalities related to a crash involving Tesla’s Full Self-Driving system.
Our research group develops holistic safety assurance methods for AI-enabled CPSs to reduce deployment risks and strengthen societal confidence in these systems. Our long-term goal is to use these methods to develop safe systems.
To achieve this goal, we study the safety assurance lifecycle for AI-enabled CPSs, which connects system and safety specifications to evidence from system execution through the four stages shown below.
- Define system and safety specifications. These can draw on safety standards such as ISO/PAS 8800 or on analyses of execution data from sources such as road traffic and maritime traffic datasets.
- Generate safety assessment artifacts. Use the specifications to derive executable artifacts, such as test cases and scenarios, for assessing system safety.
- Execute the assessment artifacts. Run the test cases and scenarios with the system, often in simulation environments such as CARLA and Gazebo, to collect data on system behaviour.
- Analyze execution data. Identify where the system meets or falls short of its safety requirements and feed the findings back into earlier stages to refine the assurance process.
Ongoing Research lines
Three research lines (RLs) are underway in our group, each addressing a different aspect of safety assurance for AI-enabled CPSs. For each line, we describe the problem that motivates it and summarize our progress so far.
RL1. Automated generation of consistent safety assessment artifacts
To meaningfully evaluate the system and safety specifications, the resulting safety assessment artifacts must be consistent with the constraints those specifications impose. In this line of research, we develop neuro-symbolic approaches that combine large language models (LLMs) with formal verification to support the generation of consistent artifacts from natural language specifications.
- Consistent string generation. We use Z3 and Python checkers to support LLM generation of strings that satisfy natural language requirements [MO2RE 2025] [RE 2025].
- Planning with probabilistic guarantees. We combine LLM-based generation with probabilistic model checking to generate plans for self-adaptive systems in uncertain environments [LLMTrust 2026] [arXiv 2026].
- Semantics-augmented constrained decoding. We ensure token-level consistency in LLM outputs by extending constrained decoding with semantics-aware analyses based on partial models and attribute grammars [arXiv 2026] [arXiv 2026].
- Traceability through structured arguments. We guide LLM generation with structured arguments to connect specifications, generated artifacts, and verification evidence [arXiv 2026].
RL2. Scenario-based testing for autonomous vehicles
Scenario-based testing evaluates the driving stack of an autonomous vehicle (AV) in generated traffic scenarios to uncover safety issues. In this line of research, we develop scenario concretization methods that turn abstract specifications into executable scenarios for testing across diverse operating conditions and traffic situations.
- Scenario concretization. We generate simulation-ready scenes from arbitrary abstract specifications and extend this approach to support exhaustive coverage of potentially dangerous manoeuvre combinations at road junctions [TSE 2024] [SoSyM 2026].
- Tool support. We developed Concretize, a model-driven tool that generates and simulates traffic scenarios from abstract specifications [MODELS 2024] [GitHub].
RL3. Automated repair of CPS requirements
As CPSs and assurance artifacts evolve, its requirements can become faulty, outdated, or ambiguous. In this line of research, we feed the results of execution data analysis back into the assurance lifecycle to repair formal CPS requirements and restore consistency with the system’s behaviour.
- Requirements repair in Simulink. We developed a framework that repairs requirements written in MATLAB Simulink Requirements Tables and uses user-defined desirability metrics to choose among valid repairs [FSE 2026].