FRET

NASA Ames’ Formal Requirements Elicitation Tool (FRET) is an open source tool for writing, understanding, formalizing, and analyzing requirements.

../_images/fret_tool_dashboard.png

The FRET user interface

The purpose of FRET is to:

  1. Make the writing, understanding, and debugging of formal requirements as natural and intuitive as possible,

  2. Seamlessly connect to powerful external tools for analysis, and

  3. Support the correction of requirements suggested by analysis results.

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 an intuitive, restricted, natural language called “FRETish” with precise unambiguous meaning. For each FRETish requirement, FRET produces natural language and diagrammatic explanations of its exact meaning, formalizes the requirement in future-time and past-time temporal logic, and supports interactive simulation of produced logic formulas to ensure that they capture user intentions. Once requirements are expressed in FRETish, FRET can then perform realizability analysis of requirements for identifying conflicts. Realizability is a notion of requirements consistency in the face of any expected input from the environment. FRET can also connect to external analysis tools by exporting requirements in a variety of formats for analysis tools such as Cocosim, Simulink Design Verifier, Kind, and SMV.

Why use FRET?

FRET and Doorstop are two open source requirements tools that are used with Space ROS. The intention is to integrate and leverage the strengths of each tool. Doorstop, along with git, is used to ensure requirements tracking and traceability, while FRET is used for requirements formalization and analysis. To facilitate interoperability, FRET is able to import and export the Markdown-based requirements file format used by Doorstop. Requirements can be stored in a git repository and operated on by either FRET or Doorstop.

To learn more about how FRET is used in Space ROS, please refer to this tutorial on the Requirements Tools and Processes used in Space ROS.

Additional References

To learn more about FRET, the following resources are available: