NASA Logo, National Aeronautics and Space Administration


FRET logo

FRET: Formal Requirements Elicitation Tool

Requirements engineering is a central step in the development of safety-critical systems. The objective of this project is to: 1) to make the writing, understanding, and debugging of formal requirements as natural and intuitive as possible; 2) to seamlessly connect to powerful external tools for analysis; and 3) to support the correction of requirements as suggested by analysis results. To this end, we have developed the Formal Requirements Elicitation Tool (FRET) for writing, understanding, formalizing, and analyzing requirements. FRET is available open source at https://github.com/NASA-SW-VnV/fret; a video can be accessed here.

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. 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. Moreover, FRET supports interactive simulation of produced formalizations to ensure that they capture user intentions. Through its analysis portal, FRET connects to analysis tools by facilitating the mapping between requirements and models/code, and by generating 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. Finally, FRET also supports, through its analysis portal, the consistency/realizability analysis of requirements via the JKind tool, which is very useful for identifying conflicting requirements. Realizability is a notion of requirements consistency in the face of any expected input from the environment.

Key Benefits

  • Intuitive platform for capturing precise requirements
    • Definition of requirements in a natural and intuitive way with precise unambiguous meaning
    • Understanding of requirements through explanations that clarify subtle semantic issues and through interactive simulation
    • Automatic generation of formalizations in a variety of formalisms
  • Connection to a variety of analysis tools
  • Support for requirements repair based on analysis feedback
  • Open sourced
    • FRET is completely open source, and it only depends on open-sourced libraries.
  • Highly extensible architecture
  • Focus on usability

Applications

We have added features to FRET based on experience of applying it on requirements of the NASA LADEE and BioSentinel missions. FRET is currently being evaluated for industrial use with requirements for jet engine controllers.

Publications

  • Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger, Michael W. Whalen. “From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET”. To appear at FM 2021.
  • Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Johann Schumann. "Automated formalization of structured natural language requirements". Information and Software Technology (IST) Journal, Special Section on REFSQ’20.
  • Hamza Bourbouh, Marie Farrell, Anastasia Mavridou, Irfan Sljivo, Guillaume Brat, Louise A. Dennis, Michael Fisher. Integrating Formal Verification and Assurance: An Inspection Rover Case Study. NFM 2021.
  • Anastasia Mavridou, Hamza Bourbouh, Dimitra Giannakopoulou, Tom Pressburger, Pierre-Loic Garoche, Johann Schumann. “The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained”, RE 2020.
  • Aaron Dutle, Cesar A. Munoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, Thomas Pressburger. "From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project", FMAS 2020.
  • Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Johann Schumann. "Generation of Formal Requirements from Structured Natural Language", REFSQ 2020.
  • Anastasia Mavridou, Hamza Bourbouh, Pierre Loic Garoche, Dimitra Giannakopoulou, Thomas Pressburger, Johann Schumann: “Bridging the Gap Between Requirements and Simulink Model Analysis”, REFSQ 2020, Poster Paper.
  • Dimitra Giannakopoulou, Anastasia Mavridou, Thomas Pressburger, Julian Rhein, Johann Schumann, Nija Shi. “Formal Requirements Elicitation with FRET”, REFSQ 2020, Tool Paper.
  • Updated 29 September 2018


    Latest News

    August 2021: FRET Team Releases Public Version 2.0 of FRET!

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

    Active Members

    Andreas Katis
    Anastasia Mavridou
    Thomas Pressburger
    Johann Schumann
    Khanh Trinh

    Past Members

    David Bushnell
    Dimitra Giannakopoulou
    Nija Shi

    Interns

    Milan Bhandari
    Kelly Ho
    Tanja de Jong
    George Karamanolis
    David Kooi
    Jessica Phelan
    Julian Rhein
    Daniel Riley

    First Gov logo
    NASA Logo - nasa.gov