日経サイエンス  2006年9月号

欠陥を見逃すな ソフトウエア設計検証ツール

D. ジャクソン(マサチューセッツ工科大学)

 11年前に新設されたデンバー国際空港の自慢は,技術の粋を尽くした旅客荷物自動運搬システムになるはずだった。総延長40kmに及ぶコンベヤー上を荷物が高速かつ途切れなく流れ,航空機あるいは旅客へと自動的に届けられる。しかし,ソフトウエアに問題が発生し解決に手間取ったあげく,開港は1年4カ月延期され,費用は予算を数億ドルも超過してしまった。

 

 開港後も改善への努力が続けられたが,結局満足に運行できず,昨年夏,ついにシステムの電源が落とされた。荷物は今,従来通り人間の手でカートに積まれ運ばれている。このシステムを設計したBAEオートメイテッド・システムズは破綻,最大の顧客だったユナイテッド航空は,これが一因となって破産した。

 

 これは特殊な例ではない。現在もお粗末なソフトウエアは数多くあり,日々,何百万というユーザーが憤懣やるかたない思いを強いられている。デンバー国際空港以外にも,米内国歳入庁(1997年のシステム改革に40億ドル,続く更新プロジェクトも80億ドルを投入して断念),米連邦捜査局(1億7000万ドルかけた事件管理システムが2005年に失敗),米連邦航空局(旧式の航空管制システムの改良に手間取り,いまだに完成していない)など,枚挙にいとまがない。

 

 こうした大失態が起きるのは,致命的な不整合や欠落が原因のこともあるが,多くは基本設計のあいまいさや検討不足のためだ。ソフトウエアの設計上の根本的な欠陥に気づくのが遅すぎるのだ。プログラマーがコード(コンピューターがプログラムを実行する際に用いる命令列)を書き始めてから,設計上の問題が発見される。

 

 誤った基本設計の下で部分的な改修を重ねるとコードは長くなり,設計の細部は複雑化する。だが,それは例外処理や穴を塞ぐためのつぎはぎで,一貫した原理を持たない。建物は基礎が堅牢でなければ安定した構造が得られないが,ソフトウエアも同じだ。

著者

Daniel Jackson

マサチューセッツ工科大学(MIT)コンピューター科学人工知能研究所でソフトウエア設計グループのリーダーを務める。主な研究領域はソフトウエア工学で,ソフトウエアの設計・仕様・解析,特に基幹システムを対象とする。オックスフォード大学で物理学修士号を,MITでコンピューター科学の理学修士号とPh.D.を得た。カーネギーメロン大学を経て現職。趣味は写真で,最近,ボストン郊外のニュートンフリーライブラリーで作品展を開いた。

原題名

Dependable Software by Design(SCIENTIFIC AMERICAN June 2006)

サイト内の関連記事を読む

キーワードをGoogleで検索する

モデル検査AlloySATソルバー自動解析抽象化