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
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
NASA Formal Methods 22(Pasadena, CA)
Funding Number(s)
Distribution Limits
Public Use Permitted.
Technical Review
NASA Peer Committee
Requirement analysis

Available Downloads

NameType NFM22Tutorialv5.pdf STI

Related Records

IDRelationTitle20220000049See AlsoIntegrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors20205007173See AlsoFrom Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project20210015352See AlsoFrom Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET20205000433See AlsoThe Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained20205004070See AlsoBridging the Gap Between Requirements and Simulink Model Analysis