Adventures in FRET and Specification

TL;DR

The paper addresses the challenge of turning natural-language requirements into verifiable specifications for safety-critical systems by employing NASA's FRET and its fretish language across four case studies. It demonstrates end-to-end workflows where fretish requirements drive formal specification in Event-B, Dafny, and temporal-logic formalisms, complemented by runtime verification with ROSMonitoring. The main contributions include detailed case-study insights, a taxonomy of fretish expressions, and a discussion of interoperability between formal methods, including traceability from requirements to verification conditions. The findings underscore FRET's utility in bridging stakeholders and formal methods, while also revealing current limitations (e.g., quantifiers, mode scoping) and opportunities to integrate workflows and tooling for scalable, industrial adoption.

Abstract

This paper gives an overview of previous work in which the authors used NASA's Formal Requirement Elicitation Tool (FRET) to formalise requirements. We discuss four case studies where we used FRET to capture the system's requirements. These formalised requirements subsequently guided the case study specifications in a combination of formal paradigms. For each case study we summarise insights gained during this process, exploring the expressiveness and the potential interoperability of these approaches. Our experience confirms FRET's suitability as a framework for the elicitation and understanding of requirements and for providing traceability from requirements to specification.

Figures (8)

• Figure 1: Screenshot of showing the fretish version of requirement UC5_R_1 from the Aircraft Engine Controller case study (§\ref{['subsec:enginecontroller']}). Each requirement has an ID (top left), and a diagrammatic semantics (right) is generated by the tool to help the user to understand the meaning behind the fretish requirement farrellfretting2022.
• Figure 2: Event-B specifications comprise contexts (static aspects) and machines (dynamic behaviour). Machines contain events that specify state changes.
• Figure 3: The basic structure of a method with specification constructs in Dafny.
• Figure 4: High-level overview of ROSMonitoring Ferrando20a. The configuration file guides the automatic instrumentation of the ROS system, where the nodes are modified (if necessary) and the monitor is synthesised.
• Figure 5: Mechanical Lung Ventilator: The controller state machine is labelled as Fig 4.1 in the case study document.