Formal Requirements Elicitation Tool (FRET) is a requirements engineering tool. It was developed by the NASA Ames Research Center to specify complex safety-critical systems whose failure could result in loss of life, significant property damage, or environmental harm.[3] FRET is open-source software released under the NASA Open Source Agreement.[4]
 FRET dashboard | |
| Developer(s) |
|
|---|---|
| Stable release | 3.1
/ December 15, 2023[2] |
| Written in | JavaScript |
| Operating system | Windows, Linux, OS X |
| Type | Formalizing |
| License | NASA Open Source Agreement version 1.3 |
| Website | https://github.com/NASA-SW-VnV/fret |
Background
editThe behavior and features of a system are specified by its requirements. Most requirements are written in natural languages such as English, which is easy for analysts and stakeholders to understand but cannot be checked for errors and omissions using formal methods. On the other hand, formal notations such as VDM and Z, which are precise and unambiguous, tend to be difficult for analysts and stakeholders to understand.[4][5]
As a compromise, FRET requirements are created in a controlled natural language called FRETish and converted into temporal logic.[4][5]
Uses
editFRETish requirements can correspond to variables in external code or models. FRET generates and verifies formal equivalents for each statement, allowing requirements to be imported or exported in a variety of formats including JSON.[4][6]
In FRET, processes are simulated and analyzed by interfacing with external modeling and analysis tools. The supported external tools include COCO simulator, Simulink Design, Verifier, NuSMV, and Copilot.[4][6]
See also
editReferences
edit- ^ "fret/CONTRIBUTORS.md at master · NASA-SW-VnV/fret". GitHub. Retrieved 26 November 2023.
- ^ "FRET: Formal Requirements Elicitation Tool". GitHub. Retrieved 2023-12-29.
- ^ Katis, Andreas; Mavridou, Anastasia; Giannakopoulou, Dimitra; Pressburger, Thomas; Schumann, Johann (2022). Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET. Lecture Notes in Computer Science. Vol. 13372. Springer International Publishing. pp. 490–504. doi:10.1007/978-3-031-13188-2_24. ISBN 978-3-031-13187-5. Retrieved 7 December 2023 – via Springer.
- ^ a b c d e Giannakopoulou, Dimitra; Pressburger, Thomas; Mavridou, Anastasia; Rhein, Julian; Schumann, Johann; Shi, Nija (2020). Formal Requirements Elicitation with FRET (PDF). REFSQ Workshops. S2CID 214708107. Archived (PDF) from the original on 2023-10-03. Retrieved 2023-11-29.
- ^ a b "Formal Requirements-Driven Verification". VALU3S Repository. VALU3S.
- ^ a b "fret/fret-electron/docs/_media/userManual.md at master · NASA-SW-VnV/fret". GitHub. Retrieved 2023-12-30.