PR

DSF、東証のシステムで形式手法の有用性を確認

要求定義や設計段階でエラーやミスの混入を防ぐには、どうすればいいか。有力な解の一つが形式手法(Formal Method)である。自動車や電子機器など他の工業製品(ハードウェア)と違って、ソフトウェアには融通無碍という特徴があり、だからこそ様々なハードをソフトで置き換える試みが進む。だがこの特徴がシステムの信頼性や安全性を損なう要因でもある。そこで数理論理学に基づく仕様記述によってこの問題を解決するのが形式手法、という因果関係だ(本誌2011年11月号「ソフトウェアの信頼性を根本的に高める「形式手法(Formal Method)」の本質」参照)。

形式手法の歴史は1970年代にさかのぼれるほど古く、日本でも大きなシステム事故が起きるたびに、注目されてきた。しかし、一向に普及する気配がない。実際、上記の本誌記事を読んでいなければ、「形式手法といわれても何のことか分からない」という人も多いだろう。

そうした中、この手法の普及/啓蒙を目指して、国立情報学研究所と国内ベンダー6社(NTTデータ、富士通、NEC、日立製作所、東芝、SCSK)が2009年に設立したディペンダブル・ソフトウェア・フォーラム(DSF)は、「情報系の実稼働システムを対象とした形式手法適用実験報告書」をまとめ、情報処理推進機構(IPA)のWebサイトで公開した。東京証券取引所の協力を得て、実際の情報システムの設計書に形式手法を適用。従来は後工程で見つかっていた問題を、基本設計の段階で発見することを実証したものだ。

具体的には、東京証券取引所の投資家向け情報配信システム(すでに開発済み)の設計書が対象。DSFは2011年8月から2012年3月にかけて、同システムのレビュー済み設計書の一部を「Event-B」、「SPIN」、「VDM++」といった形式仕様言語で記述し直して検証した。その結果、レビューをすり抜け、後工程で修正された問題点を13件検出した。

IPAソフトウェアエンジニアリングセンターの松田晃一所長は、「欠陥をテストや受け入れなど後工程でカバーするとプログラムの書き直しなどで、(上流工程で発見した場合の)30倍のコストがかかる。それを形式手法で回避できることを実証した意義は大きい」と語る。当然だが、コストがかかっても欠陥を排除できればまだいい。東証の上記のシステムの場合はなかったが、レビューやテストで欠陥を排除できない可能性もあるので、その面でも形式手法の利点は大きいと言える。

DSFはもう1つ、別の報告書も公開している。企業システムにおける形式手法の適用手順や典型的な記述例をまとめた「形式手法活用ガイド」だ。ただ完全に新しいものではなく、2011年7月に公開した旧版に上述の実証実験を通じて得た知見を加えたもの。同じWebページからダウンロードできる。「VDM++SPINなど形式仕様の記述例を掲載している。今後、形式手法に取り組むITエンジニアには、非常に参考になるはずだ」(同)という。

ガイド最終版が完成したことに伴い、DSFは6月に活動を終了する。参加ベンダーは今後、DSFの取り組みを自社における開発業務に生かしていくとし、「形式手法を理解し実践できる人材育成や、自社の開発方法論への組み込みを急ぐ」と口をそろえる。しかし額面通りには受け取れない。肝心の人材育成計画は「年間数人」(NTTデータ、富士通)から「10人程度」(SCSK)という控えめなものだからだ。

一体、なぜなのか?そもそもなぜこれまで形式手法が普及してこなかったのか。そこには大きく4つの理由がある。1番目は数理論理学に基づく仕様や設計記述という形式手法ならではのハードルの高さ。プログラム=論理や数学が通じるのは組み込みや科学技術計算分野であり、企業情報システムではほとんど不要である。建築でも機械でも他の工学なら数学が必須だが、企業ITにはそれが不要。だから多くのITエンジニアは数理論理学が苦手であり、形式手法=難解な手法となる。「実際には、数理論理学は基礎的なもので問題ない。重要なのはシステムの要件や仕様を論理に落とす、つまりモデリングのスキル。これがうまくいかない」(国立情報学研究所の中島震教授)。

第2がユーザー(発注)サイドの理解のなさ。形式手法を使おうと使うまいと、レビューやテストを厳密に実施し、結果として稼働すれば問題ない。仮にバグがあっても瑕疵担保責任で修正すればいい、というスタンスが普通だ。一般企業の情報システムならまだしも、交通や金融など社会インフラ系のシステムも同じである。ベンダーからすれば、コストをかけて形式手法を駆使できるITエンジニアを育成しても、得られるものがないばかりか、下手をすると開発期間が短くなって工数(=売り上げ)が減ってしまう恐れもある。

第3が無理を聞いてしまうベンダーの体質。プログラム開発やテスト段階など後工程のサービス残業は当たり前で、経営管理側は現場がいかに疲弊しようと関係ない。人海戦術で乗り切ろうとするし、現場サイドもまた「システム開発は長時間労働が当然」とする。プロジェクトをうまく回すのはプロジェクトマネジャーの責務(=リーダーシップや人間力)であり、”ソフトウェア工学の発想”が存在しないのだ。

そして第4は、形式手法を教育したり理解してもらうための材料(事例や効果)がないこと。この第4の問題の解消がDSFの目的であり、今回の報告書や活用ガイドに結実した。しかし容易に分かるように、これだけでは上記1~3は解決されない。加えていえば、形式手法はコンピュータ上でのシミュレーションも必要であるため、開発マシンの計算能力も必要だった(現在ではこの問題は解消されている)。

一方、形式手法発祥の地である欧州では、自動車、電気や精密機器など組み込み系のソフト開発に形式手法が広がっており、企業や行政機関のシステムについても「(停止が許されない)重要システムに関しては、形式手法の適用を強制する法制化の動きがある」(IPAの松田所長)。これに対し、日本は大きく立ち後れた。組み込みソフト開発において形式手法を適用するケースは出始めているものの、企業システム開発への適用はほとんど進んでいない。

そんな中で欧州における法制化の動きが日本に波及するのを待ってから取り組むのか、それともプロアクティブに動くのか。ベンダーだけではなく、企業や行政機関など発注者の問題意識も問われているといえそうだ。

Webサイトの記事の一部は、IT Leaders 雑誌版、電子雑誌版から転載しています。

» IT Leaders 雑誌版、電子雑誌版 無料購読お申し込みはこちら。