システムの信頼性向上をテーマに活動する業界団体「ディペンダブル・ソフトウェア・フォーラム（DSF）」は2012年4月20日、システム開発の品質強化に向けて「形式手法」の有効性を検証した実証実験の結果を公表した（報告書の公開ページ）。DSFにはNEC、NTTデータ、SCSK、東芝、日立製作所、富士通のベンダー6社と国立情報学研究所が参加している。実験は2011年8月から2012年3月にかけて実施した。

　形式手法とは、数学理論を基にしたある規則に沿って、ソフトやハードの仕様を厳密に記述し、検証する手法のこと。仕様上の矛盾やあいまいな部分を洗い出すことで、実装段階でのトラブルを未然に防ぐ効果がある。これまで主に組み込み分野で利用されてきたが、DSFは一般の業務システムにも適用できるとして普及促進を図ってきた。

　今回の実証実験では東京証券取引所が構築した業務システムの一部分について、実際の基本設計書を形式手法で書き換え、内容の整合性を検証。その結果、設計書の修正が必要な部分を22カ所発見した。

　うち13カ所は、この基本設計書を使った現実のシステム開発プロジェクトにおいて、実装やテストの段階で見つけ出したものと一致していた。つまり、もし形式手法を基本設計のレビューに活用していれば、実装・テストより上流工程となる設計段階で発見できたことになる。

　実験には、独立行政法人 情報処理推進機構（IPA）を通じ2011年7月に公開した「形式手法活用ガイド」を適用した。これは形式手法を業務システムの開発プロセスで利用するためのガイドライン。DSFは今回の結果をこのガイドラインに反映し、本日から最終版として公開している。

　参加ベンダー各社は今後、形式手法に精通した人材の育成や開発ツールの整備を進め、高信頼性が求められるシステム開発案件などでガイドラインや形式手法の活用を図っていく。