Announcing NASA’s Formal Requirements Elicitation Tool (FRET) v3.0!

[anmavrid]

Hello everyone!

We are thrilled to announce FRET v3.0, a framework for specifying, formalizing, understanding, and analyzing system requirements. FRET allows users to express requirements in restricted English, ensuring unambiguous specification. To enhance understanding of semantics, it automatically translates requirements into multiple representations, including natural language descriptions, formal mathematical logic, and diagrams.

FRET supports hierarchical structuring and exporting in various formats, enabling integration with formal analysis tools. Additionally, it features built-in consistency checking, facilitating early verification and validation (V&V) to detect potential issues at the specification stage - helping users ensure correctness from the start.

What’s new in FRET v3.0?

• Probabilistic Requirement Specification & Formalization
  The FRETish language now includes a probability field, enabling direct specification of probabilistic constraints. These requirements are automatically formalized into Probabilistic temporal logics formulas in a compositional manner, ensuring extensibility and maintainability. Furthermore, the generated formulas align with the PRISM property specification language (https://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction), facilitating smooth connection several probabilistic model checkers.

• Requirement-Based Test Case Generation
  FRET v3.0 also introduces automated test case generation based on FRETish requirements. We’ve integrated Kind 2 (https://kind2-mc.github.io/kind2/) and NuSMV (https://nusmv.fbk.eu/) engines to support past-time and future-time LTL formulas. Test cases can now be directly exported in JSON format. Additionally, the LTLSIM simulator has been enhanced, enabling users to visualize and validate the generated tests interactively. This streamlined workflow ensures comprehensive testing based on the FLIP coverage metric (https://dl.acm.org/doi/abs/10.1145/1572272.1572279)

• Other enhancements: https://github.com/NASA-SW-VnV/fret/releases/tag/v3.0.0

For details on this release, see: https://github.com/NASA-SW-VnV/fret/releases/tag/v3.0.0

This release is a collective effort from the entire FRET team - many thanks to @andreaskatis, @JohannSchumann, @tpressburger and @kvtrinh! We also thank our summer intern Gricel Vazquez (@Gricel-lee), for her valuable contributions.

Additionally, we sincerely appreciate everyone who has used FRET and engaged with us through GitHub issues, discussions and email messages. Special thanks to @anaisac, @kquick, @mariefarrell, @mluckcuck, @pcyac21, @rreis, @shamblett and @smithdtyler for your valuable feedback - it has been instrumental in improving FRET!

Finally, we are excited to announce that we now have a process in place to accept code contributions from external participants. If you are interested, feel free to reach out to us!

Thank you all,
Anastasia