ソフト開発に数理論理学を適用する「形式手法」、DSFが活用ガイドを公開

　株式会社NTTデータ、富士通株式会社、日本電気株式会社（NEC）、株式会社日立製作所（日立）、株式会社東芝と、大学共同利用機関法人 情報・システム研究機構 国立情報学研究所（NII）が参加するディペンダブル・ソフトウェア・フォーラム（DSF）は24日、エンタープライズ市場向けソフトを対象とした初めての「形式手法活用ガイド」を公開した。

　DSFは、利用者が安心して利用できる可用性、信頼性、安全性、機密性、完全性、保守性といった複合的要件を満たしたディペンダブル・ソフトウェアの実現を目指し、2009年12月に発足した団体。数理論理学を基盤に、対象システム・ソフトの機能や振る舞いについて、正確な記述と系統的な検証を行う「形式手法」に着目。形式手法適用評価ワーキンググループ（FMAWG）を立ち上げ、実際の開発現場で有効に活用できる形式手法の適用事例や適用ノウハウの蓄積、形式手法を適用したシステム開発の可能性の追求などを進めてきた。

　今回の形式手法活用ガイドは第1弾の活動成果。形式手法は、エンタープライズ系ソフト開発に適用する場合のコストが膨らむという固定概念と、活用できる技術者不足のため、適用事例が少なく、その効果も一般に公開されていないという。そこでDSFでは、適用効果を確かめるべく記述実験を行い、形式手法がエンタープライズ系ソフト開発上流工程における誤り発見に効果があることを確認。具体的に、レビューによって誤りが除去されたと考えられる設計書を形式手法で記述し直すことで、「複数の設計書で書かれている内容の矛盾」や「仕様の解釈が複数ある」といった誤りを見つけ出せたとしている。

　同時に上記実験の結果、形式手法の実務への適用には、1）現場利用を踏まえた適用手順や体制、2）形式手法を用いる際の定石や作法の知識、3）形式手法に関するスキルや教育方法、4）より現実的な開発場面での効果や利点・欠点――が重要な課題であると判明。このうち、1）～3）の課題について、以下のような対策を検討した。

　1）に対しては、エンタープライズ系ソフト開発の設計工程に対して、形式手法の適用手順をまとめた。2）に対しては、開発で想定される一般的な設計書の形式記述作成方法に対して典型的な解決例一覧と、一部、具体例を含む詳細な書き方の解決例を記述した。3）に対しては、スキル教育で必要なスキルマップやセミナープログラムを設定し、DSFメンバーを対象としたセミナーを実施して評価した。

　形式手法活用ガイドにはこれらの内容が盛り込まれている。「エンタープライズ系ソフトを開発するプロジェクトメンバーが実際に開発場面に形式手法を導入する際の参考になると期待している」（DSF）。

　今後は、課題4の「より現実的な開発場面での効果や利点・欠点」の対策として、開発現場により近い場面を想定し、形式手法の有効性を評価する実証実験を企画するという。また、今回公開した成果を実証実験で利用するために、イディオム集の充実、形式手法適用手順のさらなる具体化などの改善を進め、実証実験を通して成果の妥当性や形式手法の効果実証を図り、2011年度末に実験結果を反映させた最終成果を公開する予定としている。