Software:FRET

From HandWiki
Formal Requirements Elicitation Tool
Ghghbhbh.png
FRET dashboard
Developer(s)
  • Milan Bhandari
  • David Bushnell Tanja de Jong
  • Dimitra Giannakopoulou
  • Kelly Ho
  • George (Yorgo)
  • Karamanolis
  • David Kooi
  • Jessica Phelan
  • Julian Rhein
  • Daniel Riley
  • Nija Shi
[1]
Stable release
version 3 / 30 August 2023[2]
Written inJavaScript
Operating systemWindows, Linux, OS X
TypeFormalizing
Website

Formal Requirements Elicitation Tool (FRET) was developed by the NASA Ames Research Center to specify safety-critical applications whose failure could result in loss of life, significant property damage, or environmental harm[3]. However, since it is open-source software, FRET is available to anyone who wants to create precise, unambiguous requirements for their applications[4].

Software requirements document what the software should do. A critical first step to delivering reliable, secure, functional software is eliciting and documenting requirements. Most requirements are written in natural languages such as English, which is easy for analysts and users to understand but cannot be checked for errors and omissions using formal methods. On the other hand, formal, mathematical notations such as VDM and Z which are precise and unambiguous are very difficult for analysts and users to understand. As a compromise, FRET requirements are created using a controlled natural language called FRETish which ensures precise, unambiguous requirements that analysts and users can still understand.

FRET helps users write FRETish requirements, generates formal equivalents, and pinpoints problems using simulations and external analysis tools.

Example requirements and templates

FRET includes a set of example requirements and templates to aid users in understanding FRETish and using FRET.


Import/Export

FRET allows requirements to be imported or exported in a variety of formats to allow interfaces with other tools as well as external analysis tools.

External analysis tools

FRET provides access to process modeling tools that pinpoint timing issues and bottlenecks before any code is written. The supported external tools include COCO simulator, Simulink Design Verifier, Kind, and SMV.

See also

Formal methods

References