FRET (программное обеспечение)
FRET (Formal Requirements Elicitation Tool, что можно перевести как «Инструмент формализации требований») — программное средство для инженерии требований. Разработано Исследовательским центром Эймса (ARC) для спецификации комплексных критически важных систем, отказ которых может привести к человеческим жертвам, значительному ущербу имуществу или окружающей среде[1]. FRET распространяется как программное обеспечение с открытым исходным кодом под лицензией NASA Open Source Agreement[2].
Общие сведения
| FRET | |
|---|---|
| Тип | средство формализации требований |
| Авторы | Andreas Katis, Anastasia Mavridou, Tom Pressburger, Johann Schumann, Khanh Trinh |
| Разработчики | Andreas Katis, Anastasia Mavridou, Tom Pressburger, Johann Schumann, Khanh Trinh |
| Написана на | JavaScript |
| Операционные системы | Windows, Linux, macOS |
| Последняя версия | 3.1 (15 декабря 2023) |
| Лицензия | NASA Open Source Agreement версия 1.3 |
| Сайт | github.com/NASA-SW-VnV/f… |
Контекст
Поведение и характеристики системы определяются её требованиями. Большинство требований пишутся на естественных языках, таких как английский, что удобно для аналитиков и заинтересованных сторон, но не позволяет выявлять ошибки и пропуски с помощью формальных методов. Формальные же нотации, такие как VDM и Z, хотя и обладают точностью и однозначностью, как правило, затруднительны для понимания теми же пользователями[2].[3]
В качестве компромисса в FRET используются требования, создаваемые на контролируемом языке под названием FRETish, которые автоматически преобразуются во временную логику[2].[3]
Использование
Требования, оформленные на языке FRETish, могут быть сопоставлены с переменными во внешнем коде или моделях. Для каждой спецификации FRET генерирует и проверяет формальные эквиваленты, поддерживая импорт и экспорт требований в различные форматы, включая JSON[2].[4]
В FRET процессы моделируются и анализируются путём взаимодействия с внешними моделями и анализаторами. К поддерживаемым внешним инструментам относятся COCO simulator, Simulink, Design, Verifier, NuSMV и Copilot[2][4].
Примечания
