NTRS - NASA Technical Reports Server

Back to Results
Capturing and Analyzing Requirements with FRETFRET is an open source tool, developed at NASA Ames, 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. FRET helps users write FRETish requirements both by providing grammar information and examples during editing, but also through English and diagrammatic explanations to clarify subtle semantic issues. For each requirement, FRET automatically produces formalizations and supports interactive simulation of produced formalizations to ensure that they capture user intentions. Through its analysis portal, FRET connects to analysis tools by exporting verification code. Currently FRET connects to (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. FRET also supports the consistency/realizability analysis of requirements for identifying conflicting requirements. In this tutorial, we introduce FRET and learn to speak and analyze FRETish through several examples.
Document ID
Acquisition Source
Ames Research Center
Document Type
Anastasia Mavridou
(KBR (United States) Houston, Texas, United States)
Date Acquired
May 16, 2022
Subject Category
Mathematical And Computer Sciences (General)
Computer Programming And Software
Meeting Information
Meeting: NASA Formal Methods 22
Location: Pasadena, CA
Country: US
Start Date: May 24, 2022
End Date: May 27, 2022
Sponsors: National Aeronautics and Space Administration
Funding Number(s)
Distribution Limits
Public Use Permitted.
Technical Review
NASA Peer Committee
Requirement analysis
No Preview Available