NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

FRET Team Releases Public Version 2.0 of Software

We are thrilled to announce the new release of NASA's Formal Requirements Elicitation Tool (FRET) v2.0, available open source on Gitbhub with the FRET User Manual. FRET 2.0 features include:

  1. Revamped Analysis Portal: The Realizability Tab supports monolithic and compositional realizability analysis; diagnosis, counterexample generation, and visualization of conflicting requirements. The Variable Mapping Tab features an improved Variable Mapping interface and generation and export of verification code for the runtime monitoring of C code through the NASA Langley Copilot tool.
  2. Improved Requirements Editing: The Template selection introduces a boilerplate FRETish (tool language) sentence in the editor, to be completed by users. Predefined templates are available, but project-specific templates can also be programmed by FRET users. The Glossary displays existing variable names in your project and enables autofill of variable names in the requirements editor. A Status flag helps bookkeeping for large projects and signifies requirements in progress, completed, requiring attention, etc.
  3. Importing & Exporting: There is added support for importing legacy requirements in .csv format. Export functionality has been extended to allow exporting requirements per project.
  4. Installation & Infrastructure: We’ve updated dependencies to be compatible with node version 14 and material-ui 4.x. And the database structure has been optimized with support for legacy FRET databases.
  5. LTLSIM Simulator: The User Interface (UI) has been updated to show FRETish requirement text and includes tooltips for the formalizations.
  6. User Manual: We’ve significantly improved the User Manual with detailed documentation of all the new features.

We hope that you enjoy using FRET, and look forward to your feedback and contributions.

BACKGROUND: Requirements engineering is a central step in the development of safety-critical systems. To this end, FRET allows users to write, understand, formalize, and analyze requirements. Users write requirements in an intuitive, restricted natural language called FRETish, with precise, unambiguous meaning. For a FRETish requirement, FRET: 1) produces natural language and diagrammatic explanations of its exact meaning, 2) formalizes the requirement in future-time and past-time temporal logic, and 3) supports interactive simulation of produced logic formulas to ensure that they capture user intentions. FRET connects to analysis tools by facilitating the mapping between requirements and models/code, and by generating verification code.

NASA PROGRAM FUNDING: System-Wide Safety (SWS) project, Airspace Operations and Safety Program (AOSP), Aeronautics Research Mission Directorate (ARMD)

TEAM: Dimitra Giannakopoulou, Andreas Katis, Anastasia Mavridou, Thomas Pressburger, Johann Schumann, and Khanh Trinh

POINT OF CONTACT: Dimitra Giannakopoulou, dimitra.giannakopoulou@nasa.gov

First Gov logo
NASA Logo - nasa.gov