The integration of AI components, particularly Deep Neural Networks (DNNs), into safety-critical systems such as aerospace and autonomous vehicles presents fundamental challenges for assurance. The opacity of AI systems, combined with the semantic gap between high-level requirements and low-level network representations, creates barriers to traditional verification approaches. These AI-specific challenges are amplified by longstanding issues in Requirements Engineering, including ambiguity in natural language specifications and scalability bottlenecks in formalization. We propose an approach that leverages AI itself to address these challenges through two complementary components. REACT (Requirements Engineering with AI for Consistency and Testing) employs Large Language Models (LLMs) to bridge the gap between informal natural language requirements and formal specifications, enabling early verification and validation. SemaLens (Semantic Analysis of Visual Perception using large Multi-modal models) utilizes Vision Language Models (VLMs) to reason about, test, and monitor DNN-based perception systems using human-understandable concepts. Together, these components provide a comprehensive pipeline from informal requirements to validated implementations.

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.

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.

The Realizable, Responsive, Unobtrusive Unit (R2U2) is a stream-based runtime monitoring framework that verifies a system’s adherence to a set of formal system requirements with minimal resource overhead, allowing for real-time, online monitoring on resource-constrained systems. Yet, a persisting challenge for deploying runtime monitors is eliciting formal specifications that accurately capture system requirements commonly expressed in ambiguous natural language; therefore, we employ NASA’s Formal Requirements Elicitation Tool (FRET) to configure R2U2 monitors from structured natural language requirements. We extend FRET to formalize requirements in Mission-time Linear Temporal Logic (MLTL) - the native specification logic of R2U2, and we provide 157 MLTL rewrite rules that reduce each of FRET’s MLTL formalizations by an average of 15 operators, or 36.05% , decreasing the resources necessary to monitor these requirements with R2U2. We also introduce a novel SMT-based proof technique for automatically proving the correctness of these rewrite rules.

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.

Techniques that leverage formalized requirements as input can automate test generation and provide coverage metrics. However, the manual process of formalizing these inputs is often unintuitive and error-prone and cannot be streamlined in an industrial setting. To this end, this paper presents a formal framework that enables the automated generation of tests from requirements written in intuitive structured natural language. Our contributions are twofold: (1) We extend prior work on requirements-based testing to account for both future and past fragments of Linear Temporal Logic (LTL), including bounded operators. Our approach is defined inductively over the extended LTL syntax and is proven sound and complete. (2) We extend two existing NASA tools that support specification of requirements in structured natural language and analysis of Matlab/Simulink models. Our extensions enhance these tools with test case generation capabilities and provide a streamlined approach to testing Matlab/Simulink models. Finally, we validate our framework using real-world case studies from Lockheed Martin and NASA.

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.

The development of autonomous systems requires a rigorous process that can guarantee a system’s reliability in critical applications. At its core, an autonomous system bases its behavior on a well-defined decision making system. In this paper, we present a methodological basis for the design, formalization and formal verification of Decision Making systems for autonomous agents. The approach is generally applicable to operational objectives that can be functionally decomposed and subsequently represented as Hierarchical Finite State Machines. As a case study, we present the application of this method to implement a Decision Making model in Simulink. Furthermore, we present how we use NASA’s FRET tool to write requirements in structured natural language and generate formal specifications that can be automatically digested by NASA’s CoCoSim tool. Finally, we present how, by leveraging CoCoSim, we perform formal verification against the Simulink model and present analysis results.

Assurance cases have emerged as a way to build trust in complex autonomous systems. Many assurance case justifications for such systems need to be constantly reevaluated based on the current system context and performance. Autonomous systems, especially those deployed in remote environments, often have a ground control system that enables monitoring and remote operations. In this paper, we propose a dynamic assurance framework that aims at connecting the assurance case with the ground control system. We use the ground control system to facilitate dynamic evaluation of quantitative assurance measures that support various justifications in the assurance case. We demonstrate the proposed dynamic assurance framework on the NASA Ames Research Center project Troupe. We use a combination of in-house and external tools to identify the assurance measures, formalize the related requirements, and generate monitors that feed the data to the external ground control system.

Verification of Programmable Logic Controller (PLC) programs requires reasoning about propositions qualified in terms of time. CERN's PLCverif, an open-source tool for the analysis of safety-critical PLC systems, uses Linear Temporal Logic (LTL) for the specification of properties. Until now, PLCverif depended on third-party tools that accept LTL specifications to perform verification. However, our experience with industrial PLC programs shows that, to overcome analysis limitations, a wide range of techniques are needed to successfully verify complex properties. In this paper, we extend PLCverif to enable PLC program verification of pure-past LTL (PLTL) safety properties with assertion-based verification tools. To this end, we take an algorithm from the runtime-monitoring domain, apply it to bounded model checking of PLC programs, and implement it in PLCverif. We extend the integration of NASA's Formal Requirements Elicitation Tool (FRET) into PLCverif to use PLTL properties generated with FRET. In addition, we leverage the program structure induced by the PLC scan-cycle for a state-space reduction. Finally, we expose the algorithm to a real-world case study of critical systems at CERN.

Mobile robots are used to support planetary exploration and safety-critical environments such as nuclear plants. Central to the development of mobile robots is the specification of complex required behaviors known as missions. In this paper, we use NASA’s Formal Requirements Elicitation Tool (FRET) to specify functional robotic mission requirements. To examine the applicability of FRET in the mobile robotics domain, we studied robotic mission patterns specified in Linear Temporal Logic (LTL). These patterns were originally derived from a large repository that included patterns from the literature and consultation with industrial experts. We extend this repository with those found during our extensive literature review. Although FRET has been successfully used in the past in case studies within the aerospace domain, mobile robot requirements present new challenges in their specification. To this end, our work provides a methodological basis for using FRET in the specification of robotic mission requirements.

Blockchain-based smart contracts enable the creation of decentralized applications, which often handle assets of considerable value. While the underlying platforms guarantee the correctness of smart-contract execution, they cannot ensure that the code of a contract is correct. Today, as evidenced by a number of recent security breaches, developers still have a hard time making contracts that work properly.Even though these incidents often exploit contract interaction, prior work on smart-contract verification, vulnerability discovery, and secure development typically considers only individual contracts in isolation. To address this gap, we introduce the VeriSolid framework for the formal verification of contracts that are specified using a abstract state machine based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify the behavior of a set of interacting contracts at a high level of abstraction. VeriSolid allows the generation of Solidity code that is functionally and behaviorally equivalent to verified models, which enables the creation of correct-by-design smart contracts. We additionally introduce a graphical notation (called deployment diagrams ) for specifying possible interactions between contract types. Based on this notation, we present a framework for the automated verification, generation, and deployment of contracts that conform to a deployment diagram. To demonstrate the applicability of VeriSolid , we translate existing Ethereum Improvement Proposal (EIP) specifications to temporal properties for two of the most popular contract interfaces: ERC20 and ERC721. We also show you how to write code for the ERC20 and ERC721 interfaces in a way that is safe, and we do this by using VeriSolid . We evaluate our framework on 726 contracts that are currently deployed on the Ethereum blockchain, which include 267 ERC20 and 459 ERC721 contracts. Our experiments indicate that 18% of ERC20 contracts and 4% of ERC721 contracts fail to satisfy the EIP specifications.

Context & Motivation: The development of software that learns has revolutionized how many systems perform. For the most part, these systems are neither safety- nor mission-critical. However, as technology and aspirations advance, there is an increased desire and need for Machine Learning (ML) software in safety- and mission-critical systems, e.g., driverless cars or autonomous space robotics. Problem: In these domains, reliability is crucial and systems have to undergo much scrutiny in terms of both the developed artefacts and the adopted development process. Central to the development of such systems is the elicitation and definition of software requirements that are used to guide the design and verification process. The addition of software components that learn, and the associated capability for unforeseen behavior, makes defining detailed software requirements especially difficult. Principal ideas/results: In this paper, we identify unique characteristics of software requirements that are specific to ML components. To this end, we collect and examine requirements from both academic and industrial sources. Contribution: To the best of our knowledge, this is the first work that presents real-life, industrial patterns of requirements for ML components. Furthermore, this paper identifies key characteristics and provides a foundation for developing a taxonomy of requirements for software that learns.

[Context & Motivation] Requirements specification and analysis is widely applied to ensure the correctness of industrial systems in safety critical domains. Requirements are often initially written in natural language, which is highly ambiguous, and as a second step transformed into a language with rigorous semantics for formal analysis. [Question/problem] In this paper, we report on our experience in requirements creation and analysis, as well as run-time monitor generation using the Formal Requirement Elicitation Tool (FRET), on an industrial case study for a Lift-Plus-Cruise concept aircraft. [Principal ideas/results] We study the creation of requirements directly in the structured language of FRET without a prior definition of the same requirements in natural language. We focus on requirements describing state machines and discuss the challenges that we faced, in terms of creating requirements and generating monitors. We demonstrate how realizability, i.e., checking whether a requirements specification can be implemented, is crucial for understanding temporal interdependencies among requirements. [Contribution] Our study is the first complete attempt at using FRET to create industrial, realizable requirements and generate run-time monitors. Insight from lessons learned was materialized into new features in the FRET and JKind analysis frameworks.

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

Developing critical software requires adherence to rigorous software development practices, such as formal requirement specification and verification. Despite their importance, such practices are often considered as complex and challenging tasks that require a strong formal methods background. In this paper, we present our work on simplifying the formal requirements specification experience for resource-constrained mission critical software through the use of structured natural language. To this end, we connect NASA’s FRET, a formal requirement elicitation and authoring tool with the Shelley model checking framework for MicroPython code. We report our experience on using these tools to specify requirements and analyze code from the NASA Ames PHALANX exploration concept.

Requirements formalization has become increasingly popular in industrial settings as an effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis tools to prove important properties, such as consistency and realizability. In this paper, we present the realizability analysis framework that we developed as part of the Formal Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of conflicts between requirements and simulation of counterexamples, and discuss results from industrial-level case studies.

Formal methods and tools have become well established and widely applied to ensure the correctness of fundamental components of industrial critical systems in domains like railways, avionics and automotive. In this Introduction to the special issue, we outline a number of recent achievements concerning the use of formal methods and tools for the specification and verification of critical systems from a variety of industrial domains. These achievements are represented by four properly revised and extended versions of papers that were selected from the 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2021).

Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool ( fret ), and the RV system Copilot . We extend fret with mechanisms to capture additional information needed to generate monitors, and introduce Ogma , a new tool to bridge the gap between fret and Copilot . With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our toolchain is available as open source.

Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool. FRET is used to specify requirements with unambiguous semantics, which are then automatically translated into temporal logic formulae Ogma generates monitor specifications from the FRET output, which are compiled into hard-real time C99. To facilitate integration of the monitors in ROS2, we have extended Ogma to generate ROS2 packages defining monitoring nodes, which run the monitors when new data becomes available, and publish the results of any violations. The goal of our approach is to treat the generated ROS2 packages as black boxes and integrate them into larger ROS2 systems with minimal effort.