　根絶できなかったバグが引き起こした問題で最も有名な事例の1つになるのが、1996年6月に打ち上げを行った宇宙ロケット「アリアン5」の1号機だ。ESA（欧州宇宙機関）が運用していたこのロケットは、打ち上げ後37秒で爆発した。その理由は、打ち上げ37秒後に舵を最大にするコマンドがモーターに送られて進路が急激に変更され、空気抵抗を受けてロケットが折れてしまったためだ。

　なぜ最大舵のコマンドが送られてしまったのか。実は、バックアップ用の慣性航法装置内部で64bitの変数を16bitに代入しており、ここでオーバーフローが発生したためだった。典型的なランタイムエラーであるが、その結果は3億7000万ドルもの大損害につながった。

「アリアン5」の事故を研究して生まれた「Polyspace」

　宇宙ロケットに限らず、ミッションクリティカルなシステムにおいてはランタイムエラーが破滅的な結果を及ぼす場合がある。こうした問題を、ホワイトボックステストとかブラックボックステストなどの動的検証で、完全に捕らえて根絶するのは困難だ。

　それもあって、自動車業界では「コーディングルールの形で、ランタイムエラーにつながる問題を根絶させよう」という取り組みがなされ、「MISRA-C」や「MISRA-C++」として広く普及している。最近では、自動車業界以外でもMISRA-C/C++が次第に利用されるようになってきている。しかし、たとえMISRA-C/C++を運用していても、ランタイムエラーを起こさないことが保障されているわけではない。

　もっと根本的に根絶する方法は無いか、という研究が冒頭のアリアン5の事故を受けて始まった。この研究では、静的検証の形で、ランタイムエラーを引き起こし得る要因を検出するという内容だった。その結果として生まれたのが、MathWorksの静的検証ツール「Polyspace」である。

　Polyspaceを使えば、静的にコードを検証して、その段階でランタイムエラーになり得る潜在的なバグに対応することができる。具体的には、オーバーフローやゼロ除算、負の値に対するシフトなどの数値的欠陥、ポインタ演算に絡む静的メモリの欠陥、メモリの開放忘れなどの動的メモリの欠陥、さまざまなプログラミングの欠陥やセキュリティの欠陥、汚染されたデータの欠陥、スレッド／プロセス間同期に関する欠陥などを、全てコードベースで確認して指摘してくれるのだ。それだけでなく、最終的にはこうした指摘を正しく修正したコードに対して、ランタイムエラーが無いことを「証明」してくれる、という機能も有している。

「Polyspace」による静的コード検証結果の画面。ランタイムエラーが無いことの「証明」状況が一目で分かり、コードを実行しなくてもマウスを合わせるだけで変数のとり得る値の範囲も示される出典：マスワークス

ハンドコードの多いミッションクリティカル機器の開発に最適

　静的なコード検証ツールは世の中に幾つも存在する。しかし、コードにランタイムエラーが無いことを「証明」してくれるツールは、Polyspaceの他にはほとんどないのが実情だ。この「証明」こそが、宇宙／防衛、医療機器といったミッションクリティカルな用途向けには極めて重要である。

　ミッションクリティカル機器を開発する場合、認証済みの機器やソフトウェアの再利用を求められることも多い。そのカスタマイズについては、技術者が自身の手でプログラミング（ハンドコード）することになる。どうしてもランタイムエラーなどのバグの原因になりやすいハンドコードに対して、Polyspaceは大きな威力を発揮する。

　こうしたミッションクリティカル分野を中心に、300以上の顧客が、2000以上のライセンスを利用しているPolyspaceだが、近年では自動車業界で採用する例も増えてきた。自動車業界では、自動車メーカー／ティア1サプライヤー／ティア2……という多層的なサプライチェーンを構成しているのが一般的だ。開発するコードは、さまざまなティアのものが混在しやすく、あるサブシステムが大きなシステムに組み込まれるSystem in System的な構造にもなりやすい。

　こうした大規模なシステムでは、ランタイムエラーが発生した場合、その影響の大きさもさることながら、問題の特定とその修正に多大な時間とコストが掛かってしまう。これを避けるためには、全てのティアで納入前にPolyspaceを使い、問題が無いことを証明できる状態まで持ってゆくことで、テスト段階からの大幅な手戻りを未然に防ぐことが可能になる。

　また、自動車向けならISO 26262、一般産業機器向けならIEC 61508といった機能安全規格についても、これらの規格の認証の取得のために並々ならない努力が必要、という話もよく知られている。Polyspaceを利用すると、これらの認証取得に必要となるさまざまなソフトウェア検証項目を達成できる。

「Bug Finder」と「Code Prover」から構成

　Polyspaceは、バグ検出やコードメトリックスを行う「Polyspace Bug Finder」と、最終的なコードに問題が無いことを証明する「Polyspace Code Prover」から構成される。コーディングの途中ではPolyspace Bug Finderを使って細かくチェックを入れながら問題の箇所をつぶして置き、ある程度完成したらPolyspace Code Proverを使って全体のチェックを掛ける、という手法が一般的な運用法になるだろう。それぞれの製品Webサイトには、紹介ビデオやホワイトペーパーなども用意されているので、プロジェクト成果物の品質管理に悩んでいるのであればぜひ検討してほしい。