FMAS 2025

Prof. Paula Herber Prof. Paula Herber is a full professor at University of Münster, Germany. Her main research interests are quality assurance for intelligent embedded systems, test automation, and formal methods.

• Title: Integrated Formal Methods for the Verification of Cyber-Physical and Autonomous Systems
• Abstract: Cyber-physical systems pose significant challenges for formal methods, due to their inherent heterogeneity and interaction with a physical environment. In addition, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments, and an increasing demand to cope with uncertainties and unforeseen events. These developments call for the development of new theories and tools, but also for the integration of existing formal methods. In this talk, I will summarize some of our recent efforts towards developing methods for the integration of formal methods to support reusable specification and scalable verification of cyber-physical and autonomous systems

TBA

• Authors: Ishan Saxena, Bernd Westphal and Martin Fränzle
• Abstract

  Automated Driving Functions (ADFs) need to comply with spatial properties of varied complexity while driving on public roads. Since such situations are safety-critical in nature, it is necessary to continuously check ADFs for compliance with their spatial properties. Due to their complexity, such spatial properties need to be formalized to enable their automated checking. Scene Graphs (SGs) allow for an explicit structured representation of objects present in a traffic scene and their spatial relationships to each other. In this paper, we build upon the SG construct and propose the Abstract Scene Graph (ASG) formalism to formalize spatial properties of ADFs. We show using real-world examples how spatial properties can be formalized using ASGs. Finally, we present a framework that uses ASGs to perform Runtime Monitoring of ADFs. To this end, we also show algorithmically how a spatial property formalized as an ASG can be satisfied by ADF system behaviour.

• Authors: Marlow Fawn and Matthias Scheutz
• Abstract

  We propose a method for combining Harmonic Control Lyapunov–Barrier Functions (HCLBFs) derived from Signal Temporal Logic (STL) specifications with any given robot policy to turn an unsafe policy into a safe one with formal guarantees. The two components are combined via HCLBF-derived safety certificates, thus producing commands that preserve both safety and task-driven behavior. We demonstrate the operation of the principles with a simple proof-of-concept implementation for an object-centric force-based policy trained through reinforcement learning for a movement task of a stationary robot arm that is able to avoid colliding with obstacles on a table top after combining the policy with the safety constraints. The proposed method can be generalized to more complex specifications and dynamic task settings.

• Authors: Reydel Arrieta Olano, Renato Neves, José Proença and Patrick Meumeu Yomsi
• Abstract

  Hybrid systems are increasingly used in critical applications such as medical devices, infrastructure systems, and autonomous vehicles. Lince is an academic tool for specifying and simulating such systems using a C-like language with differential equations. This paper presents recent experiments that enhance Lince with mechanisms for executing multiple simulation variants and generating histograms that quantify the frequency with which a given property holds. We illustrate our extended Lince using variations of an adaptive cruise control system.

• Authors: Dominik Grundt, Ishan Saxena, Malte Petersen, Bernd Westphal and Eike Möhlmann
• Abstract

  Autonomous vehicles (AVs) must be both safe and trustworthy to gain social acceptance and become a viable option for everyday public transportation. Explanations about the system behaviour can increase safety and trust in AVs. However, the integration of AI-based driving functions in AVs makes explainability challenging, as decision-making processes are often opaque. The field of Explainability Engineering addresses this challenge by designing a system’s explanation model already at design time, based on analysing requirements, operational domains, and stakeholder needs. Its goal is to provide explanations that are both correct and good, considering system implementation, the current traffic context, and explanation goals for different stakeholders. To address these challenges, we propose an approach that enables context-aware, ante-hoc explanations of (un)expectable driving manoeuvres at runtime. The visual yet formal language Traffic Sequence Charts (TSC) is used to formalise explanation contexts, as well as corresponding (un)expectable driving manoeuvres. A dedicated runtime monitoring enables context-recognition and ante-hoc presentation of explanations at runtime. In combination, we aim to support the bridging of correct and good explanation. Our method is demonstrated in a simulated overtaking.

• Authors: Delphine Longuet, Amira Elouazzani, Alejandro Penacho Riveiros and Nicola Bastianello
• Abstract

  Failures in satellite components are costly and challenging to address, often requiring significant human and material resources. Embedding a hybrid AI-based system for fault detection directly in the satellite can greatly reduce this burden by allowing earlier detection. However, such systems must operate with extremely high reliability. To ensure this level of dependability, we employ the formal verification tool Marabou to verify the local robustness of the neural network models used in the AI-based algorithm. This tool allows us to quantify how much a model’s input can be perturbed before its output behavior becomes unstable, thereby improving trustworthiness with respect to its performance under uncertainty.

• Authors: Mehrnoush Hajnorouzi, Astrid Rakow and Martin Fränzle
• Abstract

  The ever-increasing level of automation in human-centered systems leads to a demand for advanced design methods for automation control at the human-machine interface. The complex, multi-layered interaction between the automated system and the human must be thoroughly checked, especially in safety-critical applications, to identify potential risks to overall safety. This requires a strategy that not only optimizes the capabilities of the automation, but also takes into account the variability of human input. In this paper, we present a model-based approach for development of a shared control that takes into account human behavior and the impact of automation on humans. The approach is based on a cognitive architecture that is transformed into a finite-state automaton through active model learning. The abstraction is then integrated into a game-theoretic framework ai med at control synthesis for automation with respect to safety requirements. The learned model is incrementally refined until it represents a sufficiently precise model of human interaction.

• Authors: Marcela Gonçalves dos Santos, Sylvain Hallé and Fabio Petrillo
• Abstract

  Industrial robotic systems (IRS) are increasingly deployed in diverse environments, where failures can result in severe accidents and costly downtime. Ensuring the reliability of the software controlling these systems is therefore critical. Mutation testing, a technique widely used in software engineering, evaluates the effectiveness of test suites by introducing small faults, or mutants, into the code. However, traditional mutation operators are poorly suited to robotic programs, which involve message-based commands and interactions with the physical world. This paper explores the adaptation of mutation testing to IRS by defining domain-specific mutation operators that capture the semantics of robot actions and sensor readings. We propose a methodology for generating meaningful mutants at the level of high-level read and write operations, including movement, gripper actions, and sensor noise injection. An empirical study on a pick-and-place scenario demonstrates that our approach produces more informative mutants and reduces the number of invalid or equivalent cases compared to conventional operators. Results highlight the potential of mutation testing to enhance test suite quality and contribute to safer, more reliable industrial robotic systems.

• Authors: Diana Benjumea Hernandez, Marie Farrell and Louise Dennis
• Abstract

  Deploying autonomous robots in safety-critical domains requires architectures that ensure operational effectiveness and safety compliance. In this paper, we contribute the Safe-ROS architecture for developing reliable and verifiable autonomous robots in such domains. It features two distinct subsystems: (1) an intelligent control system that is responsible for normal/routine operations, and (2) a Safety System consisting of Safety Instrumented Functions (SIFs) that provide formally verifiable independent oversight. We demonstrate Safe-ROS on an AgileX Scout Mini robot performing autonomous inspection in a nuclear environment. One safety requirement is selected and instantiated as a SIF. To support verification, we implement the SIF as a cognitive agent, programmed to stop the robot whenever it detects that it is too close to an obstacle. We verify that the agent meets the safety requirement and integrate it into the autonomous inspection. This integration is also verified, and the full deployment is validated in a Gazebo simulation, and lab testing. We evaluate this architecture in the context of the UK nuclear sector, where safety and regulation are crucial aspects of deployment. Success criteria include the development of a formal property from the safety requirement, implementation, and verification of the SIF, and the integration of the SIF into the operational robotic autonomous system. Our results demonstrate that the Safe-ROS architecture can provide safety verifiable oversight while deploying autonomous robots in safety-critical domains, offering a robust framework that can be extended to additional requirements and various applications.

• Authors: Mahdi Etumi, Hazel Taylor and Marie Farrell
• Abstract

  In the development of safety and mission-critical systems, including autonomous space robotic missions, complex behaviour is expressed during the requirements elicitation phase. Requirements are typically expressed using natural language which is ambiguous and not amenable to formal verification methods that can provide robust guarantees of system behaviour. To support the definition of formal requirements, specification patterns provide reusable, logic-based templates. However, there remains a gap between the natural language requirements and logical specification patterns. Tools like NASA's Formal Requirements Elicitation Tool (FRET) aim to bridge this gap. A suite of robotic specification patterns, along with their FRET formalisation already exists in the literature. These pre-existing requirement patterns are domain agnostic and, in this paper we seek to explore their applicability for space missions. To achieve this we carried out a literature review of existing space missions and formalised their requirements using FRET, contributing a corpus of space mission requirements. We categorised these requirements using existing specification patterns which demonstrated the applicability of existing patterns in space missions. However, not all of the requirements that we formalised could be assigned an existing pattern so we have contributed 5 new requirement specification patterns as well as several variants of the existing and new patterns. We also conducted an expert evaluation of the new patterns, highlighting their benefits and limitations.

• Authors: Angelo Ferrando
• Abstract

  Assuring the safety and trustworthiness of autonomous systems is particularly difficult when learning-enabled components and open environments are involved. Formal methods provide strong guarantees but depend on complete models and static assumptions. Runtime verification (RV) complements them by monitoring executions at run time and, in its predictive variants, by anticipating potential violations. Large language models (LLMs), meanwhile, excel at translating natural language into formal artefacts and recognising patterns in data, yet they remain error-prone and lack formal guarantees. This vision paper argues for a symbiotic integration of RV and LLMs. RV can serve as a guardrail for LLM-driven autonomy, while LLMs can extend RV by assisting specification capture, supporting anticipatory reasoning, and helping to handle uncertainty. We outline how this mutual reinforcement differs from existing surveys and roadmaps, discuss challenges and certification implications, and identify future research directions towards dependable autonomy.