The BDI (Belief-Desire-Intention) agent paradigm has been used to model decision-making in autonomous systems that operate with little to no human intervention, reasoning with beliefs, desires, and intentions on-the-fly to achieve goals. Since BDI agents are used to make decisions in safety-critical systems, verifying that they make correct decisions is vital. Existing design-time verification techniques are effective before deployment, but they cannot capture how agent behaviour evolves during execution, especially under imprecise actuation and probabilistic decision-making. This paper bridges the gap between design-time and run-time verification of probabilistic BDI agents. We propose a run-time quantitative operational monitoring methodology based on Discrete-Time Markov Chains (DTMCs), integrating execution traces with probabilistic model checking. Our approach constructs a DTMC representation of possible agent behaviours at design time, then incrementally updates it using observed execution traces to provide situational insight into agent operation. To demonstrate our work, we contribute a probabilistic BDI language extension, explicate our approach through smart manufacturing for probabilistic BDI agents, and use a rover case study to show the generality of our DTMC-based monitoring. We further implement this monitoring mechanism and evaluate its efficiency and scalability experimentally. This advances agent verification from pre-deployment analysis to ongoing quantitative assurance under uncertainty.

We consider the problem of engineering autonomous intelligent agents that are capable to responsibly not comply with user requests. We argue that machine non-compliance comes in many different forms, and sketch the issues we should pursue on the road of accomplishing responsibly non-compliant intelligent machines. We anchor responsible non-compliance in justifications for task refusal, pathways to override the non-compliance, as well as careful tracking of security risks and liability transfers.

Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches that can cope with, and preferably take advantage of, this inherent modularity. This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS), where each node is specified using First-Order Logic (FOL) assume-guarantee contracts that link the specification to the ROS implementation. We introduce inference rules that facilitate the composition of these node-level contracts to derive system-level properties. We also present a novel Domain-Specific Language, the ROS Contract Language, which captures a node's FOL specification and links this contract to its implementation. RCL contracts can be automatically translated, by our tool Vanda, into executable monitors; which we use to verify the contracts at runtime. We illustrate our approach through the specification and verification of an autonomous rover engaged in the remote inspection of a nuclear site, and finish with smaller examples that illustrate other useful features of our framework.

Systems deployed for long periods of time in dynamic environments may experience performance degradation that affects timing guarantees, even when their functional behaviour remains unchanged. In the design and verification of critical systems, such timing guarantees are often expressed using Metric Temporal Logic (MTL). Under degradation, these specifications may no longer hold as stated, although weaker variants that relax timing bounds may still be satisfied and remain meaningful. For example, while an elevator may initially be required to arrive within 30 s of a request, degradation of its motor may only allow us to guarantee arrival within 60 s. Although weaker, this guarantee is still useful and allows the system to maintain a reasonable level of operation. In this paper we present CEGIW, an iterative, counterexample-guided algorithm for automatically weakening timing intervals in MTL specifications so that they hold for a given system model. The algorithm preserves the logical structure of the original specification and weakens only interval bounds. We prove the correctness and optimality of CEGIW, and conduct an empirical evaluation to demonstrate the practicality of interval weakening using formalised requirements from a number of real-world case-studies. Using a model checker to produce counterexamples, CEGIW either identifies the strongest interval weakening under which the specification holds, or determines that no such weakening exists.

Formal methods enable the verification of system behavior against requirements that are expressed as formal, mathematical properties. However, translating the often ambiguous natural language requirements that are typically produced by developers and engineers into precise mathematical specifications remains a significant bottleneck in the formal verification process. NASA’s Formal Requirements Elicitation Tool (FRET) is an open source tool that addresses this challenge by bridging the gap between natural language requirements and formal specifications that are suitable for automated verification. FRET enables practitioners to express requirements in FRETish, a structured natural language, that balances intuitive readability with formal rigor. FRET automatically translates these requirements into formal properties that verification tools can directly process. This tutorial paper introduces FRET and guides readers through expressing requirements in FRETish. We present the tool’s key analysis capabilities, including simulation, realizability checking, test-case generation, and automated generation of verification conditions for external formal verification tools. Our goal is to provide a comprehensive guide that helps practitioners, regardless of their formal methods background, to effectively leverage FRET in their verification and validation (V V) workflows.

This document summarises the ABZ 2026 case study challenge. The system under consideration is that of an autonomous planetary rover. We summarise the architecture for the rover, its requirements and the tasks that participants in the case study track should focus on. We also outline several extensions that may be considered in future work or that offer other perspectives for formal modelling and verification.

Autonomous systems are increasingly deployed in safety- and mission-critical domains where humans and robots must operate as a team to complete complex tasks. Existing requirements for Human-Robot teamwork remain fragmented across disparate sources, with no unified framework that addresses complexities of collaborative Human-Robot tasks. We address this gap by presenting a taxonomy of Human-Robot Teamwork (HRT) requirements derived from analysis of (academic and industrial) literature, standards and regulatory guidance. We extracted a construction corpus of 361 requirements from 14 cross-domain sources. Through iterative classification and refinement, we develop a two-level hierarchical taxonomy comprising 6 high-level categories and 21 low-level subcategories that distinguish information provision, relational control, decision support, safety mechanisms, performance monitoring, and foundational system capabilities. We validate the taxonomy through expert evaluation with 5 domain specialists and a utility demonstration on an independently assembled corpus of 448 requirements drawn from 19 sources spanning six HRT domains.

Formal verification of autonomous systems is well established for safety and liveness analysis, yet the explicit modelling and verification of adversarial behaviour at the system level remains limited. In particular, attacker behaviour is often encoded implicitly, obscuring the distinction between attacker capability and system response. This paper presents a security-minded, state-based modelling approach in which the system and the attacker are represented as separate transition systems that interact exclusively through shared inputs. This separation preserves semantic clarity, enables compositional reasoning, and supports rigorous security analysis using standard model-checking techniques. The approach is demonstrated on an autonomous space docking system. An attacker transition system is systematically derived from CAPEC-148 (Content Spoofing) and models image-spoofing attacks against a vision-based navigation subsystem. Security countermeasures are modelled as constrained variations of the system transition semantics. Security properties are specified in LTL and verified using the SPIN model checker. The results show that explicit separation of system and attacker transition systems enables the identification of insecure configurations and the formal verification of mitigation effectiveness, providing design-time security assurance for autonomous systems.

The Belief–Desire–Intention (BDI) paradigm is a popular framework in the development of autonomous systems. However, assuring the correct design of BDI agents remains difficult: existing modelling formalisms often require ad-hoc encodings of BDI agents that can be difficult to validate, maintain, and reason about. This paper focuses on modelling the syntax of BDI agents and shows how algebraic modelling in Event-B theories (e.g. inductive data types and polymorphic constructors) yields a faithful, compact, and reusable encoding of BDI syntax. Even without committing to the full BDI semantics, the encoding already supports useful reasoning, including belief entailment and belief-based invariant checking, and provides a path towards a future BDI semantic encoding via operators in theories and machine events in Event-B.

In this paper, we present a catalogue of refactorings for formalised requirements, which improve the structure of requirements without changing their behaviour. As a requirements set evolves and grows in complexity, refactoring is needed to improve clarity, eliminate repetition, and restructure requirements without introducing errors. We integrate our approach with the formal requirement language fretish, and we implement the approach in our Mu-FRET tool. Our approach provides a rigorous grounding for refactoring formalised requirements with guarantees of semantic preservation between requirements before and after refactoring. To this end, Mu-FRET uses the Metric Temporal Logic (MTL) semantics that underpins fretish requirements to formally verify that refactoring has preserved the underlying meaning of the requirements; which is not possible for natural-language requirements. We demonstrate and evaluate our contributions on a range of complex and industry-scale use cases from safety–critical domains including aerospace and medical devices.

Engineering reliable autonomous systems is an important and growing topic in computer science. As autonomous systems become more prevalent, easy-to-use techniques for building them reliably are increasingly important. This workshop report captures and expands on the discussions at the Lorentz Center Workshop "Engineering Reliable Autonomous Systems" (ERAS), held from 10 to 14 June 2024. The workshop was co-organised by the organisers of the Workshop on Formal Methods for Autonomous Systems (FMAS) and the Workshop on Agents and Robots for reliable Engineered Autonomy (AREA). It brought together members of the FMAS and AREA communities, industry practitioners, and representatives from sectors where autonomous systems pose distinctive engineering challenges. The workshop focused on three main research topics: techniques for verification and validation of autonomous systems; engineering real-world autonomous systems; and software architectures for safe autonomous systems. Its main outcome is a catalogue of challenges in these areas and, most importantly, a pathway to solutions. Some challenges can already be tackled by techniques that are well known in academia but have not yet become regularly used in practice. Other challenges remain unresolved and require further research. This roadmap is intended to support future research and industrial collaboration.

Integrating autonomous and adaptive behavior into software-intensive systems presents significant challenges for software development, as uncertainties in the environment or decision-making processes must be explicitly captured. These challenges are amplified in safety- and mission-critical systems, which must undergo rigorous scrutiny during design and development. Key among these challenges is the difficulty of specifying requirements that use probabilistic constructs to capture the uncertainty affecting these systems. To enable formal analysis, such requirements must be expressed in precise mathematical notations such as probabilistic logics. However, expecting developers to write requirements directly in complex formalisms is unrealistic and highly error-prone. We extend the structured natural language used by NASA's Formal Requirement Elicitation Tool (FRET) with support for the specification of unambiguous and correct probabilistic requirements, and develop an automated approach for translating these requirements into logical formulas. We propose and develop a formal, compositional, and automated approach for translating structured natural-language requirements into formulas in probabilistic temporal logic. To increase trust in our formalizations, we provide assurance that the generated formulas are well-formed and conform to the intended semantics through an automated validation framework and a formal proof. The extended FRET tool enables developers to specify probabilistic requirements in structured natural language, and to automatically translate them into probabilistic temporal logic, making the formal analysis of autonomous and adaptive systems more practical and less error-prone.

Belief-Desire-Intention (BDI) architecture is a popular framework for designing autonomous systems. As these systems make independent decisions and execute actions independent from humans, ensuring their safety and reliability becomes a major concern. Traditional verification methods often fail to give run-time operational insights into an agent's behaviours, especially with quantitative assessments under uncertain conditions, such as imprecise actuating. Meanwhile, BDI agents, which rely on context-sensitive subtask expansion, act as they go e.g. selecting plans at run time. To address this, we have developed a monitoring method that combines real-time operational data with probabilistic verification. This approach allows us to quantitatively analyse the decisions of BDI agents as they occur to understand the impact of each decision as it happens.

[Context and motivation] Software requirements are commonly expressed in natural-language, which must be formalised if they are to be used by formal methods such as Runtime Verification (RV), where we verify that an implementation obeys its requirements during execution. [Question/problem] This paper reports on our experience of using the Formal Requirements Elicitation Tool (FRET) to formalise requirements for an autonomous tilt-rotor drone in the ProVANT Emergentia research project. Structured, formalised requirements help to refine the meaning of, and discover ambiguities in, a requirements set, which is beneficial for safety-critical systems. FRET generates a temporal logic semantics for each requirement, providing formulas that can be used for RV. [Principal ideas/results] We describe the process of formalising the natural-language requirements using FRET. We present the progress made in each of the four versions of the requirements set as new information was elicited and incorporated. Our two concrete outputs are the formalised requirement set, which we will use in our ongoing development and verification of ProVANT; and metrics about the requirements. [Contribution] From our experience, we present guidance for requirements elicitation and formalisation with FRET. We highlight situations where it was difficult to formalise these requirements and describe potential improvements to FRET to address these difficulties.

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.

[Context & Motivation] Explainable autonomous systems are increasingly essential for engendering trust, especially when they are deployed in safety-critical scenarios. [Question/Problem] Despite the robust reliability needed in critical settings, there remains a gap between Explainable AI and Requirements Engineering (RE), raising the question: can current RE techniques sufficiently elicit explainability requirements and what characteristics do these requirements have? [Principal Ideas/Results] We examine whether established RE techniques can be used to elicit explainability requirements and analyse the characteristics of such requirements. We answer these questions in the context of a nuclear robotics case study focused on navigation and task scheduling missions. [Contribution] We contribute: (1) an experience report of eliciting explainability requirements, (2) categories for explainability requirements for explainable autonomous robotic systems and (3) practical guidance for applying our approach in other safety-critical domains.

There are many forms of human-robot teamwork, ranging from scenarios in which humans act as supervisors, monitoring the robot’s behavior and stepping in when necessary, to more collaborative situations where humans and robots work together seamlessly. In these cooperative setups, a robot may handle specific manual tasks while the human focuses on others, complementing each other’s strengths to achieve a common goal. Throughout this spectrum of teamwork, it is of utmost importance that the robot is able to explain its actions to the human involved. This is to maintain safety and ensure that the robot does not take incorrect actions. Human-robot teams are increasingly desired in hazardous and, often, highly regulated domains where requirements engineering plays a crucial role in the development process. However, requirements for human-robot teams and the explainability features that are needed present a gap in the literature. To fill this gap, we present a novel catalog of explainability requirement patterns for human-robot teamwork. Our pattern catalog addresses the identified gap by incorporating human-centered features and providing reusable templates. This catalog is derived from real-world industrial use cases, demonstrating its applicability and effectiveness in meeting explainability needs in critical domains. To aid verification and understanding, we formalize these patterns using NASA’s Formal Requirements Elicitation Tool (FRET) which provides a logical semantics for each pattern.

Formal methods have been employed for requirements verification for a long time. However, it is difficult to automatically derive properties from natural language requirements. SpecVerify addresses this challenge by integrating large language models (LLMs) with formal verification tools, providing a more flexible mechanism for expressing requirements. This framework combines Claude 3.5 Sonnet with the ESBMC verifier to form an automated workflow. Evaluated on nine cyber-physical systems from Lockheed Martin, SpecVerify achieves 46.5% verification accuracy, comparable to NASA's CoCoSim, but with lower false positives. Our framework formulates assertions that extend beyond the expressive power of LTL and identifies falsifiable cases that are missed by more traditional methods. Counterexample analysis reveals CoCoSim's limitations stemming from model connection errors and numerical approximation issues. While SpecVerify advances verification automation, our comparative study of Claude, ChatGPT, and Llama shows that high-quality requirements documentation and human monitoring remain critical, as models occasionally misinterpret specifications. Our results demonstrate that LLMs can significantly reduce the barriers to formal verification, while highlighting the continued importance of human-machine collaboration in achieving optimal results.