クラスターミッション

クラスター(Cluster)は、欧州宇宙機関がアリアン5ロケットの処女飛行で打ち上げた4機の人工衛星の集合体であるが、ロケットは軌道に到達しなかった。打上げは1996年6月4日に行われたが、表明が切れていたことによる整数のオーバーフローによるソフトウェアの設計ミスによる失敗に終わった。このため、ロケットは打上げから37秒後に軌道を外れ、高い空気力の下で分解し始め、自動自爆装置により破壊された。この失敗は、歴史上最も悪名高く高くついたバグの1つとして知られるようになった。この失敗により、3億7000万ドル以上が無駄になったと言われている。
人工衛星.
クラスターは、224Wの太陽電池で給電される、1200kgの円筒形のスピン安定性人工衛星4機で構成されている。4機は四面体を構成するように飛行し、地球の磁気圏の調査を行うことを目的とする。軌道は、短径17200km、長径120600kmの高楕円軌道で、軌道傾斜角は赤道に対し90°である。
打上げの失敗.
アリアン5は、アリアン4の慣性航法装置を再利用しているが、アリアン5の飛行経路は前のモデルとはかなり異なる。特に、アリアン5の水平方向に大きな加速は、バックアップも含めたコンピュータを破壊して診断データを消失させ、オートパイロットに偽の位置と速度を誤認させた。アリアン5の飛行条件下の慣性飛行試験は行われなかったため、打上げ前には、このエラーは発見されなかった。事故原因調査において、別の慣性航法装置を用いてアリアン5の模擬飛行が行われたが、実際と同じように失敗した。
水平方向に大きな加速は、64ビット浮動小数点数から16ビット符号付き整数値へのデータの変換を引き起こし、算術オーバーフローしたことで例外処理された。効率化のため、このような個々の変数の範囲確認は省略されていたが、コード中の他の変数の変換については保護されていた。例外処理は参照プラットフォームを停止し、飛行の破壊につながった。
報告書は、ソフトウェアのバグを直接の原因と認定しているが、別の調査ではシステム設計や運用の問題を指摘しているものもある。
算術オーバーフロー.
事故原因の調査に加わったJean-Jacques Levyによると、問題を引き起こしたAdaのソースコードは以下のようなものであった。
L_M_BV_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BV) * G_M_INFO_DERIVE(T_ALG.E_BV));
if L_M_BV_32 > 32767 then
 P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elsif L_M_BV_32 < -32768 then
 P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
 P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
end if;
P_M_DERIVE(T_ALG.E_BH) := 
 UC_16S_EN_16NS (TDB.T_ENTIER_16S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH)));
最終行（ここでは2行となっている）がオーバーフローの原因となり、ここで64ビットから16ビットへの変換は保護されていなかった。正しいコードは以下のようになる。
L_M_BV_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BV) * G_M_INFO_DERIVE(T_ALG.E_BV));
if L_M_BV_32 > 32767 then
 P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elsif L_M_BV_32 < -32768 then
 P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
 P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
end if;
L_M_BH_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH));
if L_M_BH_32 > 32767 then
 P_M_DERIVE(T_ALG.E_BH) := 16#7FFF#;
elsif L_M_BH_32 < -32768 then
 P_M_DERIVE(T_ALG.E_BH) := 16#8000#;
else
 P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BH_32));
end if;
言い換えると、垂直方向の計算(E_BV)に既に実装されていたものと同じオーバーフローチェック機構が水平方向の計算(E_BH)にも実装されるべきであった。
その後.
失敗の後、4機のクラスターIIが建造された。これらは、2000年に2機ずつソユーズU/フレガートによって打ち上げられた。
打上げの失敗は、大衆、政治家、会社役員等に、複雑なコンピューティングシステムに関連した高いリスクへの認識をもたらし、生命に関わるシステムへの信頼性を確保する研究への支援が増加した。その後行われたアリアン5のソースコードの自動解析は、抽象解釈による大規模な静的コード解析の初めての事例となった。
この失敗は、アリアン4の高い成功率によって打ち立てられた欧州宇宙機関のロケットの成功記録にも傷を付けた。アリアン5の打上げがアリアン4と同等の信頼性を持つと認められたのは、2007年になってからであった。
出典.
Thomas, L.D. (2007) Selected Systems Engineering Process Deficiencies and their Consequences. Acta Astronautica, 61, 406-415.