HOME | products | T-VEC | 形式手法・定理証明・テストベクタ自動生成事例

火星探査機の事故は T-VEC で回避できていた

The Mars Polar Lander (MPL)

形式手法・定理証明・テストベクタ生成の実践的事例


 
 
T-VEC をベースにしたテスト自動化フレームワーク(TAF)による著名な成果の一つに、Mars Polar Lander (MPL 火星無人探査機) の事故解析事例がある。NASAは、1994年2月7日にMPLプロジェクトを着手し、6年後の1999年12月3日、MPLは3500万マイル以上の飛行をし、予定された着陸まで数分のところで、地上との交信が途絶えてしまった。この開発と打ち上げには、1億6500万ドルが費やされていた。
我々は事故後、TAFでバグを検出することができるかを、調査する機会を得た。そこで、あえてコードを見ることなく、SCR手法を基にしたツールで、要求仕様書を TTM にモデル化し、テストを自動生成させた。具体的にはTouchdown Monitor (TDM 着地モニター)の要求仕様を、TTMにモデル化し、MPLの着陸手順に関連するソフトウエア上のエラーを、24時間以内に発見することができた。
 

MPL was launched on January 3, 1999 and lost on December 3, 1999

 

 
TDMは、火星へMPLが降下する時の2つ段階で、3本の着陸脚の状態をモニターするソフトウエアコンポーネントである。図にあるように、TDMモジュールを、1秒当たり100回、リアルタイムなマルチタスク実行がコールし、着陸脚センサーからの情報を2つ目のモジュールから受け取る。これら2つのモジュールはTDMへのインターフェイスを構成している。火星上空およそ5Kmから開始される降下第一段階で、TDMソフトウエアは、3本の着陸脚をモニターする。

各着陸脚には1つのセンサーがあり、これによって脚が着地したことを確認する。各着陸脚を所定の位置に固定するときに、反動でセンサーが誤った着地信号を示す課題は想定されていた。そこでTDMソフトウエアは、この想定されたイベントに対し、2回連続で誤った信号を読み取ると、その着陸脚のセンサーを不良として、マーキングする。 そして、火星上空およそ40mから開始される降下第二段階で、TDMソフトウエアは、残りの正常なセンサーをモニターする。 その後、1つのセンサーから着地を知らせる2回連続の信号を読み取ると、TDMソフトウエアは、降下エンジンを停止する。
MPLに何が起こったか、絶対的な確認手段は無い。考えられているのは、1つ以上のセンサーから、上空40mに達する前(第一段階)に、2つの連続した信号を読み取り、その着陸脚センサーの情報がTDMプログラムメモリに保持されていたこと。そしてMPLが上空40mに達したとき、TDMの状態が変更され、降下第一段階の着陸脚センサーに相当するメモリを読んだ。そしてメモリが2回連続の信号読み取りを示し、エンジンスラスタが火星上空40mで停止されたと、開発エンジニアは確信している。様々な方法で要件のデザインと実装を行えるが、この設計上の本質的な欠陥は、プログラム変数が、不良センサーの情報を保持していたこと。(そしてプログラム上にエラー(バグ)を誘発した)