[最前線]

2011年11月7日(月)藤本 洋

リスト

ITが広く社会に浸透し、個人の生活や企業活動にとって不可欠な役割を担うようになって久しい。それだけにITに対する信頼性や安全性の要求は、かつてないほどに高まっている。ひとたび障害が発生すれば、多くの個人や企業に甚大な影響を及ぼすからだ。

例えば、銀行のオンラインシステムや航空機の予約システムがダウンすれば、預金の引き出しや搭乗手続き、計画通りの運航が困難になり、多数の人が影響を受ける。自動車の電子制御システムに問題が生じれば、最悪の場合、人命を危機にさらす。

このような背景から、システム稼働時の信頼性を高める様々な試みがなされている。システムを構成する機器の冗長化は、その1つ。障害から自律回復する技術の研究やシステムのダウンタイムを減らすための工夫も重ねられている。開発においても同様に、テストに莫大な工数を費やしたり、ミスやエラーを徹底的に排除したりする試みがなされている。こうした取り組みが運用や開発の工程で着々と広がるのに対し、上流の工程、すなわち仕様策定における信頼性向上の取り組みはあまり進んでいないのが実情だ。

以下では、まず信頼性の低い仕様が生まれてしまう原因を考察する。そのうえで仕様の信頼性を高める手段として注目を集め始めている「形式手法（Formal Method）」について解説する。

あいまいさや多重下請けなど仕様を詰め切れない理由

システムのユーザーレビュー時や稼働直前、あるいは稼働後しばらくしてから「何かが違う」という意見がユーザーから噴出し、「仕様を詰め切れなかった」と反省した経験がないだろうか。仕様を詰め切れない理由はいくつも存在する。

初期のあいまいなニーズや暗黙知

仕様に考慮漏れや矛盾がないことが、高品質なソフトウェアを開発する大前提であることは言うまでもない。だが、現実には“完璧”な仕様を策定するのは難しく、潜在的な不備を潰せないまま、次工程に進むケースが多い。もちろん単なる人為的ミスが仕様漏れを招くこともあるが、画面操作時の応答時間のように、ユーザーが実際に動かしてみるまで決定しにくい要件も少なくない。

「暗黙知」も無視できない存在だ。仕様を策定する担当者のスキルが高いために無意識のうちに仕様から記述が省略されるケースはよくある。設計者や開発者が同水準のスキルや知識、経験を持つなら問題は少ないが、そうでなければ暗黙知が仕様の不備に直結する可能性がある。

改訂に伴う仕様の劣化

レビューなどにより発覚した仕様ミスの修正や、仕様書や設計書の改訂作業時に発生する「仕様の劣化」も大きな問題の1つである。日本語で定性的に記述した仕様の一部を改定した場合、その影響範囲を正確に把握することは容易ではない。当然、レビューによって確認されるが、所詮は人手の作業のため、仕様の改定を重ねるにつれて仕様書全体の整合性が低下していくのが常である。

多重下請け構造

ソフトウェア開発は、ある種の“分業体制”で成立している。具体的には、ユーザー企業から開発を受注した1次受けの技術者が要件をまとめ、それを下請けや派遣社員に割り振る。そして下請けから上がってきたプログラムを検収してユーザー企業に納品する。

要件に見合った成果物を納品するには、発注者と1次受け、下請けが一様に正確な作業内容を共有することが欠かせない。しかし、仕様書や設計書は自然言語による記述を多かれ少なかれ含んでいる。そのため作業内容はあいまいになり、手戻りや不具合、信頼性の低下をもたらす。スキルの割りに人件費が安いオフショア開発を活用する際、整合性の低下問題はより深刻となるだろう。

ソニーのFelicaでも活用
あいまいさを取り除く形式手法

上述したように、仕様を詰め切れない理由は多岐にわたるが、すべてに共通しているのは、自然言語で記述することによるあいまいさの存在である。裏を返せば、あいまいさを徹底的に排除し、誰が見ても解釈がぶれない記述ができれば仕様が抱える問題を解決できる。それを可能にする手段として今、改めて形式手法に注目が集まっている。

おそらく本誌読者の相当数は、形式手法という言葉に聞きおぼえがあるだろう。1980年代に主にヨーロッパで研究が広がり、電子マネー「Felica」に適用したソニーのケースなど国内でも複数の実用例がある。ただ、形式手法の実態はそれほど知られていないように思われる。

そこで改めて形式手法の基本を整理すると同時に、形式手法を用いた仕様策定のアプローチを見ていきたい。実際にシステム開発プロジェクトに適用するかどうかはともかく、IT責任者や担当者にとって知っておいて損はないはずだ。

数学的な概念を使い仕様を表現
実体は基本的な集合と論理

形式手法では数学的な概念を用いて対象を表現する。具体的には、主に「集合」と、集合や集合の要素同士の「関係」を用いて対象を表現する。そして複数の集合や関係に対して何らかの操作をした場合に、それらの関係が「成り立つ」もしくは「成り立たない」という言明を「論理命題」の形で表す。このように「論理」を数学的に扱う学問分野は「数理論理学」と呼ばれ、形式手法は主にその中で研究されてきた。

数学というと、小難しい話に聞こえるかもしれないが、決して複雑ではない。むしろ単純といったほうが正しい。形式手法で扱うのは、「And、Or、Not、->、Exist、All」のような論理演算と、「集合、関係、関数」といった基本的な数学概念が中心となる。

「集合や論理で多様なシステム（プログラム）の機能要件や非機能要件を記述できるのか?」という疑問が聞こえてきそうだが、結論を言えば、Yesだ。もちろんシステムはダイナミックに変化するので、状態遷移モデルを作ったり、andやorで構成した論理式に時間的な順序関係を表現する演算子をいくつか導入した「時相論理（temporal logic）」と呼ばれる記述を使用したりもする。

そのための「形式仕様記述言語（記述言語）」もそろっている。代表格に挙げられるのがVDMやZ記法、さらにはB-Methodで用いられるB-抽象機械などだ。これらを用いれば数学表現と同等の内容を記述し、仕様の正しさを検証できるようになる。