FRET (software)

La Herramienta de Obtención de Requisitos Formales ( FRET ) es una herramienta de ingeniería de requisitos . Fue desarrollada por el Centro de Investigación Ames de la NASA para especificar sistemas complejos de seguridad crítica cuyo fallo podría provocar la pérdida de vidas, daños materiales significativos o daños ambientales. ^{[ 3 ]} FRET es un software de código abierto publicado bajo el Acuerdo de Código Abierto de la NASA . ^{[ 4 ]}

Fondo

El comportamiento y las características de un sistema se especifican mediante sus requisitos . La mayoría de los requisitos se redactan en lenguajes naturales como el inglés, que son fáciles de entender para analistas y partes interesadas , pero no permiten detectar errores ni omisiones mediante métodos formales . Por otro lado, las notaciones formales como VDM y Z , que son precisas e inequívocas, suelen ser difíciles de comprender para analistas y partes interesadas. ^{[ 4 ]}^{[ 5 ]}

Como solución de compromiso, los requisitos FRET se crean en un lenguaje natural controlado llamado FRETish y se convierten en lógica temporal . ^{[ 4 ]}^{[ 5 ]}

Usos

Los requisitos de FRET pueden corresponder a variables en código o modelos externos . FRET genera y verifica equivalentes formales para cada enunciado, lo que permite importar o exportar requisitos en diversos formatos, incluido JSON . ^{[ 4 ]}^{[ 6 ]}

En FRET, los procesos se simulan y analizan mediante la interfaz con herramientas externas de modelado y análisis. Las herramientas externas compatibles incluyen el simulador COCO , Simulink Design, Verifier, NuSMV y Copilot. ^{[ 4 ]}^{[ 6 ]}

Véase también

Referencias

↑ "fret/CONTRIBUTORS.md en master · NASA-SW-VnV/fret" . GitHub . Consultado el 26 de noviembre de 2023 .
↑ "FRET: Herramienta de obtención de requisitos formales" . GitHub . Consultado el 29 de diciembre de 2023 .
↑ 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. Consultado el 7 de diciembre de 2023 – vía Springer.
1 2 3 4 5 Giannakopoulou, Dimitra; Pressburger, Thomas; Mavridou, Anastasia; Rhein, Julian; Schumann, Johann; Shi, Nija (2020). Formal Requirements Elicitation with FRET (PDF) . REFSQ Workshops. S2CID 214708107. Archivado ( PDF) del original el 3 de octubre de 2023. Recuperado el 29 de noviembre de 2023 .
1 2 "Verificación basada en requisitos formales" . Repositorio VALU3S . VALU3S.
1 2 "fret/fret-electron/docs/_media/userManual.md en master · NASA-SW-VnV/fret" . GitHub . Consultado el 30 de diciembre de 2023 .

[1] "fret/CONTRIBUTORS.md en master · NASA-SW-VnV/fret" . GitHub . Consultado el 26 de noviembre de 2023 .

[2] "FRET: Herramienta de obtención de requisitos formales" . GitHub . Consultado el 29 de diciembre de 2023 .

[3] 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. Consultado el 7 de diciembre de 2023 – vía Springer.

[refsq-4] 1 2 3 4 5 Giannakopoulou, Dimitra; Pressburger, Thomas; Mavridou, Anastasia; Rhein, Julian; Schumann, Johann; Shi, Nija (2020). Formal Requirements Elicitation with FRET (PDF) . REFSQ Workshops. S2CID 214708107. Archivado ( PDF) del original el 3 de octubre de 2023. Recuperado el 29 de noviembre de 2023 .

[valu3s-5] 1 2 "Verificación basada en requisitos formales" . Repositorio VALU3S . VALU3S.

[usermanual-6] 1 2 "fret/fret-electron/docs/_media/userManual.md en master · NASA-SW-VnV/fret" . GitHub . Consultado el 30 de diciembre de 2023 .

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]