ディペンダブル・ソフトウェア・フォーラム（DSF）は4月20日、障害を起こさないソフトウェア（Dependable Software）を開発するための「形式手法」（Formal Methods）の活用ガイドを改訂、最終版を公開した。
形式手法は、数理論理を基礎に対象とするシステムやソフトウェアの機能、振る舞いを正確に記述し、系統的に検証する手法・技術の総称。対象を厳密に記述することで、要求や設計の矛盾、抜け漏れなどの誤りに気付くことができるという。ツールを活用して検証することで、要求や設計仕様の矛盾、抜け漏れなどの誤りも発見できるとされている。
DSFは2009年に発足。NTTデータ、富士通、NEC、日立製作所、東芝、SCSKといった民間企業のほかに、国立情報学研究所が参加している。障害を起こさないソフトウェアを開発するために形式手法に着目。開発現場への形式手法導入を支援する活用ガイドを2011年7月に公開している。活用ガイドは、形式手法の適用手順や典型的な形式記述の例をまとめている。
情報処理推進機構（IPA）は、形式手法の利用が進んでいない原因として、参考となる形式手法を適用した事例情報がないことであると考え、実運用中のシステムに形式手法を適用したときの効果と具体的な作業工数の測定を目的に実験を2011年8月から展開している。
実験は、東京証券取引所（東証）で実際に運用しているシステムの、すでにレビューが済んでいる設計書716ページに形式手法を適用した。設計書レビューでは発見できなかった指摘事項55件を抽出している。
そのうちの22件は東証が設計書を修正すべきであると評価している。この22件の指摘事項を分析すると、半数以上の13件が、実際の開発では設計書作業より後の工程で発見したことが判明している。
実験の結果から、通常の開発では実装やテストといった設計作業後の工程で見つかる指摘事項が、形式手法での検査により設計工程で見つかり、設計工程以降に発生する作業の手戻りが削減できる可能性を示すことができたという。
ページあたりの基本設計レビュー実績工数の基本統計量と比較することで、設計書の改善点発見手段として一般的に使用されているレビュー手法と形式手法とでは、作業効率的に大きな差がないことも確認している。
形式手法で発見した改善点や作業コスト、作業効率、作業者のスキル、作成した形式記述について、作業者14人（約560人時分）のデータを公開することで、形式手法導入を検討する発注者や受注者に実開発に近く、より精度の高い情報を提供できるとしている。
実験にはDSFもメンバーとして参加し、実作業を担当している。DSFは実験で新しく考案、改善した手順や記述方法をより実践的な知見として活用ガイドに取り入れ、DSFの活動の集大成として活用ガイドの最終版を公開した。
DSFは成果物の著作権を6月にIPAに譲渡する予定としている。
