FRET (software)
| 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 |
FRET (Formal Requirements Elicitation Tool, tradotto in italiano Strumento di Elicitazione dei Requisiti Formali) è uno strumento di ingegneria dei requisiti. È 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]
Contesto
[modifica | modifica wikitesto]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 | modifica wikitesto]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 | modifica wikitesto]- ^ (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.
