別紙

IPAでは、ソフトウェアおよびシステムの安全性・信頼性の確保を重要な課題と捉え、形式手法の普及を含めたさまざまな取り組みを行っています。

本実験はそのような活動の一環として、IPA　技術本部ソフトウェア・エンジニアリング・センターの統合系システム・ソフトウェア信頼性基盤整備推進委員会が設置した「形式手法技術部会ワーキンググループ（形式手法適用実証WG）」において2011年8月から2012年3月にかけて実施したものです。実験の題材には、東京証券取引所で実際に開発されたソフトウェアの設計書を使用し、本ガイドの2011年7月21日公開版に沿って設計書の検査に形式手法を適用しました。

本実験は、東京証券取引所で実運用中のシステム設計書延べ716ページを対象に、設計作業終了直後の設計書の内容を形式手法で記述、検証を行い、55件の指摘事項を抽出しました。そのうち、22件の指摘事項は、東京証券取引所が設計書を修正すべきであると評価したものです。また、22件の指摘事項を分析したところ、半数以上の13件の指摘事項が実際の開発では設計書作業より後の工程で発見したことが判明しました。本結果から、通常の開発では実装やテストといった設計作業後の工程で見つかる指摘事項が、形式手法を用いた検査によって設計工程で見つかり、設計工程以降に発生する作業の手戻りが削減できる可能性を示すことができました。また、ページあたりの基本設計レビュー実績工数の基本統計量^注6との比較により、設計書の改善点発見手段として一般的に使用されているレビュー手法と形式手法とでは、作業効率に大きな差がないことを確認しました。さらに本書は、形式手法で発見した改善点や作業コスト、作業効率、作業者のスキル、作成した形式記述について、作業者14名（約560人時分）のデータを公開することで、形式手法導入を検討する発注者や受注者に実開発に近くより精度の高い情報を提供します。

本実験の結果をさまざまな視点で評価するために、発注者および受注者、学識経験者が委員として本実験に参加しました。本実験の結果に対して、発注者の委員は「設計書等の品質を向上させるための方策の一つとして、従来のレビューに加えて形式手法を採用することは十分可能であると思われる」との見解を示しました。また学識経験者の委員は、形式手法の効果を確認できたことと作業工数等の具体的なデータを得られたことを評価しました。これらの評価は実際に形式手法導入を検討した例として活用できるため、発注者や受注者にとって形式手法利活用の可否を判断する助けとなります。

2011年7月21日に公開した本ガイドの改訂にあたり、DSFは本実験のため新たに考案あるいは改善した手順や記述方法を本実験中に記録しました。またDSF関連のグループ会社や本実験メンバーである発注者に依頼し、本ガイドに対する全101件の改善要望コメントを収集しました。

改善要望コメントへの対応として、本ガイド中の用語や概念について解説を追加したため全ラインアップで可読性が向上しました。その他については以下表で個別に掲載します。