生死をも左右するソフトウェアの設計・構築はどうすれば完璧に近づけられるのか？

By Lwp Kommunikáció

多くの装置がコンピューターによって制御されるようになった現代では、機械そのものの安全性はもちろん、それを制御するプログラムの安全性が極めて重要です。その中でも特にコンピューターによる制御が多く取り入れられている旅客機と、技術の粋を集めた宇宙ロケットの制御ソフトウェア構築の現場では非常に高い正確性が求められるのですが、そこで取り入れられている方法や思想についてまとめられています。

How Is Critical 'Life or Death' Software Tested? | Motherboard
http://motherboard.vice.com/en_uk/read/how-is-critical-life-or-death-software-tested

多くの乗客を乗せて空を飛ぶ旅客機は、今ではその多くに「フライ・バイ・ワイヤ(FBW)」と呼ばれるコンピューター制御の飛行制御システムが取り入れられています。FBWが登場する前の機体では、パイロットが握る操縦桿やスロットルの操作は「リンケージ」と呼ばれる装置によって物理的に翼やエンジンに伝えられていたのですが、FBWを搭載した機体ではパイロットの操作は電気信号としてコンピューターに入力され、状況に応じて最適と判断した命令を電気信号として各部に伝えるという仕組みになっています。

By Jan Ottenbourg

「コンピューターが最適な判断を下してくれる」と聞くと、なんとなく心強いものを感じてしまうわけですが、それはあくまで「コンピューターのプログラムが正常に作動していること」を大前提にしたもの。ひとたび思いがけないエラーが発生して正常な判断が行われず、しかもパイロットの操作を一切受け付けないといった状態が起こってしまうと事態は一転、これほど恐ろしいものはないと言わざるを得ない状況に陥ってしまいます。

このようなリスクを軽減するため、現代の旅客機では1つの操縦システムに依存せず複数の操縦系統をバックアップとして持つ「冗長化」を行い、仮にメインのシステムにエラーが発生した場合にも瞬時に別のシステムに切り替わるというフォールト・トレラント・システムが取り入れられています。このように、システムの一部に問題が生じた場合でもこれを補って安全性を確保する設計手法はフェイルセーフと呼ばれ、事故を防ぐ上で重要な考え方となっています。

By EthelRedThePetrolHead

とはいえ、やはり最も重要なのは根本的にエラーの起きないシステムを作り上げることにあるのは言うまでもありません。旅客機に限らず、どんなプログラムでも必ず仕様どおりに動くかを確認する「デバッグ」の作業を行い、最終的な信頼性を高める手順があるのですが、ここにはさまざまな思想やスタイルが存在しています。

アメリカ・パデュー大学のジーン・スパッフォード教授はある作り話を題材に、2大航空機メーカーであるボーイングとエアバスのプログラム検証に対する考え方の違いを以下のブログで紹介しています。

CERIAS - Center for Education and Research in Information Assurance and Security

1980年代後半、ちょうど航空業界ではエアバスがA340型機のデビューを控えていた頃だが、ソフトウェア関連やセーフティ関連のエンジニアの間ではあるエピソードが有名だった。そのエピソードとは、ボーイングとエアバスという2大航空機メーカーで、FBWのテスト方法がどれだけ異なるかについてのものだった。

それによると、エアバスでは機体に搭載されるシステムを検証するために、最新かつ非常に優れた手法を取り入れ、モデル検証を行ってプログラムの形式的証明を実施した。

一方のボーイングでは、大がかりな設計審査とテストを行い、最後に全てのプログラマーを機体の初飛行の際に同乗させた。

このエピソードを聞くと、多くの人は何となくボーイング製の旅客機に多くの安心感を抱くようだ。

上記のエピソードはあくまで都市伝説的に語り継がれているものなので、実際にそのような手法が行われていたかどうかは不明ですが、両社のコンピューターシステムに対する考え方の違いをよく表しているものといえそう。ひとたび空に舞い上がった機体では、おちおち修正作業などは行うことができず、自らの命を預ける機体の開発に対する気合の入り方もおのずと変わってくるというものですが、果たしてその手法が正しいのか、あるいはエアバスのようなリスクの少ない方法が効率・安全の面で優れているのか、その答えは人ぞれぞれといえるのかも。

2011年には、オンラインQ&Aサイト「Stack Exchange」のスレッドで、そんなテスト手法についての議論が交わされており、GoogleのSEプログラマーであるウリ・デケル氏は「ここでいうボーイングのような手法は、とっくに時代遅れのものとなっています」と指摘しています。

testing - How is software used in critical life-or-death systems tested? - Programmers Stack Exchange

プログラムの分野ではボーイングの例にみるような無作為機能試験(random functional testing)から、形式的検証(formal verification)へと移る流れが絶対的なものになっているとのこと。デケル氏によると、NASAのような政府系機関や防衛産業ではこのようなテクノロジーの開発に力が注がれており、確かに一般的なプログラマーにとっては頭の痛い問題ではあるものの、特に航空機やロケットのような重大なシステムを検証する上で効率的であることが確認されているそうです。

ホームオートメーション関連のソフトウェアをオープンソースで提供するソフトウェアライブラリ「FluentDwelling」を運営するスコット・ウィットロック氏は、さらに具体的な手法を語っています。

家のカギや照明などを自動で制御する「ホームオートメーション」にとって、やはり重要なのはシステムの安全性です。仮に問題が発生しても問題なく作動するフェイルセーフの仕組みが取り入れられているわけですが、例えば2重の冗長性を持たせたシステムを構築する場合には、それぞれ別々の業者にシステムを作らせ、両社を隔離させた状態で別々にプログラム設計を行わせるとのこと。そしてできあがったそれぞれのシステムに対して同時に同じ指示を与え、同じ動作が行われない場合はそのシステムは「失敗」ということになるそうです。

多くの予算をつぎ込み、パイロットの人命を左右することにもなる宇宙開発になると、求められるレベルは一気に高くなります。Fast Companyのチャールズ・フィッシュマン氏によると、NASAのロケットに搭載されるシステムは「絶対にクラッシュしない」レベルになっているとのこと。

They Write the Right Stuff | Fast Company | Business + Innovation

フィッシュマン氏によると、そのプログラムの安定度はまさにケタ違いとのこと。「エラーによる再起動は必要とされず、バグも存在しない。人間が作り上げた中で最も完全に近いシステムです。最近の3バージョンのプログラムでは、42万行に及ぶプログラムで見つかったエラーは、それぞれ1か所ずつ。最新11バージョンで見るとその数は17個に増えています。これに対し、一般向けに開発された同じ規模のプログラムでは、エラーは5000個は存在しているでしょう」と、明らかなレベルの違いが存在する様子を語っています。

それではなぜNASAはこのようなシステムの開発が可能なのでしょうか？フィッシュマン氏はこれを「そうする必要があるから」と説明します。42万行のプログラムの中にあるほんの1文字の間違いにより、数十億ドルどいう予算が無駄になり、乗組員や地上スタッフの命をも危険にさらすということになるため、万全を期す体勢が常に求められるというのがその理由のようです。

By Steve Jurvetson

また、完璧なプログラムを作り上げることを「プログラマー」の手にゆだねていないのも理由であるとのこと。プログラムの現場では「創造性」は排除され、全てのスタッフは9時に出社して5時には退社。何でもできる「超人プログラマー」の存在は一切求められておらず、プログラムの品質を「マンパワー」ではなく「プロセス」によって高める仕組みが構築されているのが大きな理由であるとしています。

このような仕組みの上で作り上げられたプログラムは、前述の通り全くといっていいほどエラーが発生しないとのこと。エラーが見つかった場合でも、それは個人の失敗ではなく、そのような失敗を起こさせた方法にあると捉え、改善されるという思想が行き渡っているそうです。

良い仕事を行うには「段取り八分」が大切であると言われるように、事前の準備や環境作りは重要なもの。全ての状況で同じことが言えるとは限らないのは事実ですが、NASAのような取り組みを徹底して行うことで、精度の高い成果物を作り上げる仕組みが作り上げられるのかもしれません。