別紙

ニュースリリース/グループ会社

形式手法適用実証実験について

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

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

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

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

形式手法活用ガイドについて

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

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

名称 説明 前回リリース(2011年7月21日公開版)からの変更点
(1)形式手法活用ガイド 導入の手引き
  • 形式手法の概略および形式手法活用ガイドの各ラインアップの位置づけを解説します。
  • 名称を「形式手法活用ガイドの紹介」から「形式手法活用ガイド 導入の手引き」に変更しました。
  • 形式手法の効果に関する本書の記述を本ガイドに引用したため、本ガイド単独で形式手法の効果から使い方までの概要を理解できるようになりました。
(2)形式手法適用手順
  • 形式手法(VDM++注7、SPIN注8、Event-B注9)の適用手順を解説します。
  • 受注者(管理者、技術者)が形式手法を適用する際に手順を検討する参考として使用することを想定します。
  • 形式手法適用手順に記載された6手順のうち、5手順を活用して本実験を効率よく実施することができました。
  • 本実験での記述に合わせた手順の見直しを行い、実際の開発で利用できる手順として洗練しました。
  • 状況に合わせた適用手順のカスタマイズについて解説を追加したため、カスタマイズによる適用範囲が広がり、より多くの読者が使えるようになりました。
  • 形式手法支援ツールの機能や使い方について解説を追加し、またすぐにツールに入力できる形で形式記述のサンプルを提供したため、形式手法の特徴であるツールを用いた検証を素早く実体験できるようになりました。
(3)形式手法イディオム集
  • 形式手法(VDM++、SPIN、Event-B)適用手順から参照する、形式記述の典型的な表現を解説します。
  • 受注者(技術者)が形式記述を作成する際に参考として使用することを想定します。
  • VDM++編、SPIN編、Event-B編合わせて34イディオムを本実験に活用することができ、実験作業の効率化に寄与しました。
  • 本実験で使用した形式記述をイディオムとして形式手法イディオム集に追加したため、活用できるイディオムが増えました(VDM++編に3イディオム追加しました)。

注釈

  • 注6ページあたりの基本設計レビュー実績工数の基本統計量

    “SECBOOKS ソフトウェア開発データ白書 2010-2011”p.209掲載の「ページあたりの基本設計レビュー実績工数の基本統計量」のこと。

  • 注7VDM++

    VDM(Vienna Development Method)と呼ばれる形式手法で使用するオブジェクト指向形式仕様言語。集合論と一階述語論理と呼ばれる数学の概念を用いて仕様を表現し検証する。特に、作成した形式記述の型チェックやテストによってシステムが満たすべき特性を検査する。SCSK株式会社がVDM開発支援ツールのVDMToolsを無償提供している。

  • 注8SPIN

    モデル検査法と呼ぶ自動検証の方法を提供するツール。G.J.Holzmann博士が開発、無償公開しており、国内の産業界ならびに大学等の教育機関でも関心が高い。分散ソフトウェアなどの並行ソフトウェアの表現を記述すること、ならびに自動検証に向いている。調べることができる性質は「デッドロックが発生しない」といった基本的なものに加えて、線形時相論理と呼ばれる形式で表現したものがある。

  • 注9Event-B

    ソフトウェアの分析、設計を行う形式手法。集合論と一階述語論理と呼ばれる数学の概念を用いて仕様を表現し検証する。特に、仕様を段階的に詳細化、具体化する過程で正しさを検証する作業を繰り返し行う。検証すべきことの多くを自動検証できる。欧州連合(European Union)のフレームワークプログラム(FP)7支援研究プロジェクトDEPLOYが統合ツールRODINを開発し無償公開している。