[市場動向]

2012年4月27日(金)田口 潤（IT Leaders編集部）

リスト

　形式手法の歴史は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）という控えめなものだからだ。