ディペンダブル・ソフトウェア・フォーラムが成果第一弾を公開 ～エンタプライズ系で初めて形式手法活用ガイドを公開～

株式会社NTTデータ、富士通株式会社、日本電気株式会社、株式会社日立製作所、株式会社東芝の5社と、大学共同利用機関法人　情報・システム研究機構　国立情報学研究所^注1が参加するディペンダブル・ソフトウェア・フォーラム（Dependable Software Forum、略称名はDSF）は、活動成果の第一弾として、エンタプライズ^注2市場向けのソフトウェアを対象とした初めての形式手法活用ガイドを、本日よりDSF公式ホームページに公開します。本ガイドは、エンタプライズ系ソフトウェアを開発するプロジェクトメンバが実際の開発場面に形式手法^注3を導入するときの参考になると期待します。

現在、社会システムはより高信頼・高品質が求められています。また、自動車や家電等のハードウェアに組み込まれる組込み系ソフトウェアを中心に、形式手法を適用した開発を推奨する動きがあり、形式手法に注目が集まっています。そこで、2009年12月にDSFを設立し、具体的に活動するワーキンググループである形式手法適用評価WG（Formal Methods Application WG、略称名はFMAWG）の中で、形式手法適用事例、及びノウハウを蓄積してきました。

形式手法活用ガイドは、ディペンダブル・ソフトウェア^注4実現の有力な手段である形式手法を実際の開発現場で有効に活用するために、各参加企業が連携して作成しています。

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

また、同時に上記実験の結果、形式手法の実務への適用には以下4点の課題が重要であることが分かりました。

DSFは上記のうち、課題1～3について対策を検討しました。

形式手法活用ガイドの個々の説明は以下の通りです。

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

FMAWGは、ディペンダブル・ソフトウェア実現の有力な手段である形式手法に着目し、具体的な検討活動を行うワーキンググループです。FMAWGは、実際の開発現場で有効に活用できる形式手法の適用事例や適用ノウハウを蓄積・公開し、形式手法を適用したシステム開発の可能性を追求するWGです。