JAXA - 人工衛星の姿勢制御ソフトウェア

国内

ドメイン	航空運輸
開発対象	人工衛星であるSELENEおよびWINDSの姿勢制御ソフトウェア
国	日本
開発組織	JAXA (旧NASDA)
形式手法（言語、ツール）	UPPAAL
適用範囲・規模（形式手法）
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	仕様記述
実装言語	C
実装規模
効果	時間制約を考慮した検証を行うことができた

（出典: Naoki Ishihama, Hideki Nomoto, Haruka Nakao, NASDA IV&V ........., NASA IV&V Facility, 2003）

モデルの不変条件や到達性を検証した。

高信頼のシステム・ソフトウェアを実現する必要があった。

ソフトウェアの要求がデータフローチャートで記述されており、UPPAALモデルはデータフローチャートであるから、UPPAALの適用を決定した。また、時間制約を記述する必要があり、UPPAALは時間オートマトンを拡張したネットワークをモデル化することができる。

ソフトウェア成果物の妥当性を検証するチームがIV&V（独立検証および妥当性確認）の一環として実施した。

Naoki Ishihama, Hideki Nomoto, Haruka Nakao, NASDA IV&V ........., NASA IV&V Facility, 2003, http://www.nasa.gov/centers/ivv/ppt/172865main_NASDA.ppt