FRET Tutorial

Tom Pressburger; Anastasia Mavridou

NASA NTRS · 20220009659

FRET Tutorial

Abstract

In this tutorial, we present the FRET tool for writing, understanding, formalizing and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. This tutorial explains how requirements can be captured in FRETish and subsequently formalized in temporal logics and in the synchronous data flow language Lustre. We show, through multiple examples, how FRET assists users in understanding FRETish requirements and clarifying subtle semantic issues through English and diagrammatic explanations as well as interactive simulation. FInally, this tutorial describes how FRET can be used to perform realizability checking for identifying conflicting requirements and the connection of FRET with (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs.

Explore related subjects

FRET Requirements Structured Natural Language Realizability Analysis

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Tom Pressburger, Anastasia Mavridou. FRET Tutorial. https://ntrs.nasa.gov/citations/20220009659

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRS2023

From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif

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.

FRET↗

NASA NTRS2022

Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors

Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. To provide the level of assurance required for ultra-critical systems, monitor specifications must faithfully reflect the original mission requirements, which are often written in ambiguous natural language. 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 tool chain is available as open source.

FRET↗

NASA NTRS2021

Compositional Realizability Checking within FRET

A set of requirements for a reactive system is realizable if, for any sequence of inputs that satisfy the assumptions on the environment, the guarantees always hold. Realizability checking is essential to ensure that an implementation can be constructed that satisfies the requirements. We propose a framework that supports users in the non-trivial task of developing realizable requirements. Our framework uses architectural information to automatically de-compose a set of requirements into subsets that can be analyzed separately, and therefore more efficiently. It then integrates existing algorithms in order to detect unrealizability, identify minimal sets of conflicting requirements, and compute counterexamples. The capability to focus on minimal conflict sets is key for localizing and correcting the sources of unrealizability. Our approach supports this process by enabling users to interactively visualize and explore the produced conflict sets and counterexamples. We have implemented our framework in the open-source Formal Requirements Elicitation Tool (FRET), and have used it on a variety of industrial-level case studies, showcasing the strengths of our approach in terms of raw performance, as well as diagnostic potential.

FRET↗