FRET (software)
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]
| FRETFormal 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
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
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]