FRET（ソフトウェア）

Formal Requirements Elicitation Tool ( FRET ) は、要求工学ツールです。NASA エイムズ研究センターによって開発され、故障すると人命の損失、重大な物的損害、または環境被害につながる可能性のある複雑な安全上重要なシステムを規定するために使用されています。 ^{[ 3 ]} FRET は、 NASA オープンソース契約に基づいてリリースされたオープンソースソフトウェアです。^[⁴^]

背景

システムの動作と機能は、その要件によって規定されます。ほとんどの要件は英語などの自然言語で記述されており、アナリストや利害関係者が理解しやすいものの、形式的手法を用いてエラーや漏れをチェックすることはできません。一方、VDMやZなどの形式的表記法は、正確で曖昧さがない反面、アナリストや利害関係者が理解しにくい傾向があります。^{[ 4 ]}^{[ 5 ]}

妥協案として、FRET要件はFRETishと呼ばれる制御された自然言語で作成され、時間論理に変換される。^{[ 4 ]}^{[ 5 ]}

用途

FRETish の要件は、外部コードやモデルの変数に対応できます。FRET は各ステートメントの形式的な等価物を生成および検証し、 JSONを含むさまざまな形式で要件をインポートまたはエクスポートできるようにします。^{[ 4 ]}^{[ 6 ]}

FRETでは、外部のモデリングおよび分析ツールと連携してプロセスをシミュレートおよび分析します。サポートされている外部ツールには、COCOシミュレータ、Simulink Design、Verifier、NuSMV、およびCopilotが含まれます。^{[ 4 ]}^{[ 6 ]}

参考文献

↑ "fret/CONTRIBUTORS.md at master · NASA-SW-VnV/fret" . GitHub . 2023年11月26日取得.
↑ "FRET: 形式要件抽出ツール" . GitHub . 2023-12-29取得.
↑ 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-52023年12月7日取得– Springer経由。
1 2 3 4 5 Giannakopoulou, Dimitra; Pressburger, Thomas; Mavridou, Anastasia; Rhein, Julian; Schumann, Johann; Shi, Nija (2020). FRET を用いた形式的要件抽出(PDF) . REFSQ ワークショップ。S2CID 214708107 . 2023-10-03のオリジナルからアーカイブ(PDF) 。2023-11-29に取得。
1 2 「形式的要件駆動検証」 . VALU3S リポジトリ. VALU3S。
1 2 "fret/fret-electron/docs/_media/userManual.md at master · NASA-SW-VnV/fret" . GitHub . 2023-12-30に取得.

[1] "fret/CONTRIBUTORS.md at master · NASA-SW-VnV/fret" . GitHub . 2023年11月26日取得.

[2] "FRET: 形式要件抽出ツール" . GitHub . 2023-12-29取得.

[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-52023年12月7日取得– Springer経由。

[refsq-4] 1 2 3 4 5 Giannakopoulou, Dimitra; Pressburger, Thomas; Mavridou, Anastasia; Rhein, Julian; Schumann, Johann; Shi, Nija (2020). FRET を用いた形式的要件抽出(PDF) . REFSQ ワークショップ。S2CID 214708107 . 2023-10-03のオリジナルからアーカイブ(PDF) 。2023-11-29に取得。

[valu3s-5] 1 2 「形式的要件駆動検証」 . VALU3S リポジトリ. VALU3S。

[usermanual-6] 1 2 "fret/fret-electron/docs/_media/userManual.md at master · NASA-SW-VnV/fret" . GitHub . 2023-12-30に取得.

[ 3 ]

[

[ 5 ]

[ 6 ]

背景

用途

関連項目

参考文献