NASA Logo, National Aeronautics and Space Administration

FRET logo

FRET: Formal Requirements Elicitation Tool

The objective of this project is to enable the definition of requirements in a form as close to natural English as possible but which can be easily formalized so that it can be used in formal analysis.

To this end, we have developed a tool, FRET, that uses English templates for the various elements that make up requirements. Each of these templates has a corresponding formal form that can be used to translate whole requirements into logical formulae. FRET is currently able to generate formal properties in Simulink form, which can then be checked against Simulink models with the CoCoSim tool.

Key Benefits

  • Definition of formalizable requirements based on English-like patterns
  • Automatic generation of formal properties and tests
  • Customizable pattern templates for ease of use


We have evaluated FRET on requirements of NASA missions such as the LADEE mission, or the BioSentinel mission.

Updated July 2018

Latest News

April 2018: FRET is unveiled internally to the RSE community.

Active Members

Dimitra Giannakopoulou
Tom Pressburger
Nija Shi
Hank Bushnell

Related Projects

SpeAR from AFRL

First Gov logo
NASA Logo -