asahi.comに、“「のぞみ」断念で「全員が再出発必要」宇宙開発委が苦言”、と言う記事が掲載されています。日本の宇宙開発における最近の事故多発を受けて、「これらの失敗の直接原因だけでなく、（組織のあり方も含めた）踏み込んだ原因の調査と対策が必要だ」、との宇宙開発委員長の言葉があったようです。
事故が起こる度に新聞や雑誌を見ていますと、組織的な問題点や人事考課制度の問題点を指摘している記事が多いようです。精神論でロケットが飛ばせるうちはそれだけで解決するかもしれませんが、複雑なシステムになるロケットや人工衛星の場合は、もう少し科学的なアプローチが必要になるのではないでしょうか？
委員長の言葉にもあるように、失敗の直接原因の究明は当然ではありますが、それでは同じ原因による事故は無くすことができたとしても、似たような原因はごまんとありますから、いつまで経ってもシステム全体の信頼性は向上しないのではないかと思います。
最近の大規模なLSIでは、数億個にも及ぶトランジスターが相互に接続されていますが、単純な論理の変更・修正によっても、思わぬところで正しい機能を損なうコード（バグ）を作り込んでしまう危険性があります。複雑さがあるレベルを超えると、精神論では解決できない領域に入ってしまうのです。
そこでLSIの設計現場では、フォーマル・ベリフィケーションと言う手法が取り入れられています。変更・修正が正しく行われたかどうかを、システム的にモデル解析を行って検証するのです。この検証作業を行うことによって設計のエラーを検出することができ、実際のハードウェアでトラブルが起こることを未然に防ぐことができるのです。
実はこのフォーマル・ベリフィケーションは、NASAのLangley Research Centerが開発した手法なのです。
1970年代後半、航空宇宙分野でのシステムの信頼性を向上するために、NASAではSIFTと呼ばれたプロジェクトを立ち上げました。SIFTとは、Software Implemented Fault Toleranceの略で、ヒューマン・エラーがあっても正常に機能する航空宇宙分野のオペレーティング・システムの開発を目指したものでした。
このプロジェクトは結局成功しないまま終了するのですが、その成果は1988年にVIPERというプロセッサーを航空宇宙分野で採用する時に応用されました。人間の手によっては到底できない未曾有のレベルのアナリシスをシステマティックに行い、このプロセッサーの不完全さを取り除いて行ったのです。
その後、様々な検証作業にフォーマル・ベリフィケーションが採用され、スペースシャトルやGPSの検証にも使われたのです。この過程でハードウェアモデルの検証のみならず、ソフトウェアモデルの検証にも使われるようになってきます。
1990年代には、NASAの航空機制御システムの改良に採用されます。また、初期のペンティアム・プロセッサーにバグが発見されたことをきっかけにして、フォーマル・ベリフィケーションはLSIメーカーの間で広まって行きます。
2000年からの10年間で、致命的な航空機事故の８０％を削減する計画が進んでおり、航空システムを安全にするためにフォーマル・ベリフィケーションは欠かせないものになっています。
さて、LSI一つでさえも人手では検証できないぐらい複雑になって来ています。ましてやH-IIAロケットになると部品の数は28万点にも上ると言われています。どの一つの部品を取っても、設計・製造・組み立てのミスは致命的になります。これは組織を変えたら解決したりするほど簡単な事ではないのは明らかです。
日本には優れた工業技術がありますが、それに頼り過ぎると同じ程度の信頼性しか得られない可能性があります。
よく工業製品で信頼性の高いものを表す時、９９．９９９％などと言う数字が出てきますが、これは０．００１％の欠陥率、すなわち10万個に一つしか欠陥品がないと言うことです。1000個の部品を使う製品があれば欠陥率の合計は１％ですから、100個の製品のうち1つが不良品となる程度です。
しかし、同じ信頼性の部品を28万個集めると２８０％となってしまいます。単純な掛け算が正確ではないとしても、９９．９９９％の部品を使っていてはロケットは作れないと言うことが解ります。これまでの工業製品の限界を超えるための技術的なブレークスルーが必要になってきます。
これまでの事故の教訓を十分に生かし、信頼性を飛躍的に改善して行かなければ、日本の宇宙開発に明日はないでしょう。「科学無き者の最後」にならないように、あらゆる英知を結集する事が今求められているのです。