宇宙開発の命運を分ける「言葉の壁」。NASAが開発した究極の翻訳機『FRET』とは？
宇宙探査において、たった一つのソフトウェアのバグは、数千億円の損失や、時には人命の危機に直結します。
過酷な宇宙空間では、「再起動すれば直る」という地球上の常識は通用しません。
そのため、NASA（アメリカ航空宇宙局）のシステム開発には、文字通り「完璧」が求められます。
しかし、ここで開発者たちは大きな壁にぶつかります。
それは、「人間の言葉の曖昧さ」です。
「熱くなったら止める」の落とし穴
システムを設計する際、最初は人間が自然言語（英語など）で要求仕様を書きます。
例えば、「システムは、温度が高くなった場合、速やかにシャットダウンしなければならない」といった具合です。
一見すると問題ないように思えますが、コンピュータにとってこの文章は穴だらけです。
「温度が高い」とは何度からなのか？
「速やかに」とは1ミリ秒以内なのか、1秒以内なのか？
このような人間の言葉の「解釈の揺れ」が、致命的なシステムの欠陥を生み出す最大の原因となっています。
この「人間の曖昧な言葉」と「機械が求める厳格な論理」の橋渡しをするために、NASAエイムズ研究センターが開発したオープンソースの画期的なソフトウェア工学ツールが、「FRET（Formal Requirements Elicitation Tool）」です。
FRETish：曖昧さを許さない「NASAの公用語」
FRETの最大の特徴は、「FRETish（フレティッシュ）」と呼ばれる独自の記述ルールを持っていることです。
FRETishは、英語をベースにしながらも、文法や構造を厳密に制限した「制限付き自然言語」です。
FRETishでは、要件を以下の6つの要素に分解して記述します。
Scope（適用範囲）: いつ、どの状態で
Condition（条件）: 何が起きたら
Component（対象）: どのシステムが
Shall（義務）: 必ず～しなければならない
Timing（タイミング）: いつまでに
Response（応答）: 何をするか
先ほどの曖昧な要件をFRETishのルールに当てはめると、「運用モード（Scope）において、センサー温度が80度を超えた場合（Condition）、メインエンジンは（Component）、必ず（Shall）、直ちに（Timing）、シャットダウン手順を開始する（Response）」のように、極めて明確な文章に強制的に整理されます。
言葉を「数学」に変換する魔法
FRETの真の力は、ここから先にあります。
人間がFRETishで入力した要件を、FRETは裏側で瞬時に「時間論理（Temporal Logic）」と呼ばれる数学的・形式的な数式に自動変換します。
時間論理とは、「ある状態が将来必ず起こるか」「特定の条件が満たされるまで維持されるか」といった時間の流れを伴う条件を、数学的に証明するための厳密な言語です。
つまりFRETは、「人間が読み書きできる言葉」を入力すると、「コンピュータが数学的にバグがないことを証明（形式的検証）できる数式」を出力する、究極の翻訳機なのです。
自動運転や医療機器への応用も
NASAのミッションを成功に導くために生まれたFRETですが、その応用範囲は宇宙だけに留まりません。
完全自動運転車、航空機の制御システム、生命維持に関わる医療機器など、絶対にバグが許されないミッションクリティカルな分野において、FRETのような「要件の数学的検証ツール」は今後不可欠な技術となっていくでしょう。
人間の直感と、機械の完璧な論理。
FRETは、その両者を結びつけることで、私たちの社会をより安全なものへとアップデートし続けています。
