FRET (software)
FRET (Formal Requirements Elicitation Tool, tradotto in italiano Strumento di Elicitazione dei Requisiti Formali) è uno strumento di ingegneria dei requisiti. E' stato sviluppato dall'Ames Research Center (ARC) per specificare sistemi critici per la sicurezza complessi il cui guasto potrebbe comportare la perdita di vite umane, significativi danni alle proprietà o danni ambientali.[3] FRET è un software open source rilasciato sotto la licenza NASA Open Source Agreement.[4]
| FRET
Formal Requirements Elicitation Tool software | |
|---|---|
 | |
| Genere | Formalizzatore (non in lista) |
| Sviluppatore | Andreas Katis, Anastasia Mavridou, Tom Pressburger, Johann Schumann, Khanh Trinh. |
| Ultima versione | 3.1 [2] (15 Dicembre 2023) |
| Sistema operativo | Microsoft Windows Linux macOS |
| Linguaggio | JavaScript |
| Licenza | NASA Open Source Agreement versione 1.3 (licenza libera) |
| Sito web | github.com/NASA-SW-VnV/fret |
Contesto modifica
Il comportamento e le caratteristiche di un sistema sono specificati dai suoi requisiti. La maggior parte dei requisiti sono scritti in linguaggi naturali come l’inglese, che è facile da comprendere per gli analisti e le parti interessate ma non può essere controllato per eventuali errori e omissioni utilizzando metodi formali. D’altra parte, notazioni formali come VDM e Z, che sono precise e inequivocabili, tendono ad essere difficili da comprendere per gli analisti e le parti interessate.[4][5]
Come compromesso, i requisiti di FRET sono creati in una lingua controllata chiamata FRETish e convertiti in logica temporale.[4][5]
Usi modifica
I requisiti FRETish possono corrispondere a variabili nel codice esterno o nei modelli. FRET genera e verifica equivalenti formali per ogni istruzione, consentendo l'importazione o l'esportazione dei requisiti in una varietà di formati, incluso JSON.[4][6]
In FRET, i processi sono simulati e analizzati interfacciandoli con modelli esterni e strumenti di analisi. Gli strumenti esterni supportati includono COCO simulator, Simulink, Design, Verifier, NuSMV, e Copilot.[4][6]
Note modifica
- ^ (EN) fret/CONTRIBUTORS.md at master · NASA-SW-VnV/fret, su github.com. URL consultato il 26 novembre 2023.
- ^ (EN) FRET: Formal Requirements Elicitation Tool, su github.com. URL consultato il 29 dicembre 2023.
- ^ (EN) Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger e Johann Schumann, Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET, Lecture Notes in Computer Science, vol. 13372, Springer International Publishing, 2022, pp. 490–504, DOI:10.1007/978-3-031-13188-2_24, ISBN 978-3-031-13187-5. URL consultato il 7 dicembre 2023. Ospitato su Springer.
- ^ a b c d e Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Julian Rhein, Johann Schumann e Nija Shi, Formal Requirements Elicitation with FRET (PDF), REFSQ Workshops, 2020. URL consultato il 29 novembre 2023 (archiviato dall'url originale il 3 ottobre 2023).
- ^ a b (EN) Formal Requirements-Driven Verification, su VALU3S Repository, VALU3S.
- ^ a b fret/fret-electron/docs/_media/userManual.md at master · NASA-SW-VnV/fret, su GitHub. URL consultato il 30 dicembre 2023.