PRESS RELEASE

2012年4月20日
株式会社NTTデータ
富士通株式会社
日本電気株式会社
株式会社日立製作所
株式会社東芝
SCSK株式会社
大学共同利用機関法人 情報・システム研究機構 国立情報学研究所
独立行政法人情報処理推進機構

東京証券取引所の設計書を対象とした実験で形式手法の有効性を実証

実験結果をもとにDSFが「形式手法活用ガイド」を完成

概要

DSFは、ディペンダブル・ソフトウェアを実現するために、実践的、かつ系統的・論理的な設計技術を確立させる研究開発を行い、ソフトウェアに起因するシステム障害の低減を目指し活動してきました。具体的には、エンタプライズ系ソフトウェア（注4）の分野では開発現場への形式手法導入を支援するガイドが今までなかったことから、DSFは国内で初めて形式手法の適用手順や典型的な形式記述の例をまとめた本ガイドを作成し、2011年7月21日に公開しました。

また、IPAは、昨今の形式手法の利用が進んでいない原因は参考となる形式手法を適用した事例情報がないことであると考え、実運用中のシステムに形式手法を適用したときの効果と具体的な作業工数の測定を目的に、本ガイドに従って2011年8月より本実験を行いました。

具体的には、東京証券取引所で実際に運用しているシステムの、すでにレビュー実施済みの設計書に形式手法を適用したところ、設計書レビューでは発見されなかった指摘事項（注5）を発見できました。また、東京証券取引所が設計書を修正すべきであると評価した指摘事項のうち半数以上は、従来では実装やテストといった設計工程以降で発見されていたものでしたが、今回形式手法を用いた検査によって設計工程で発見できたことから、設計工程以降に発生する作業の手戻りが削減できる可能性を示すことができました。

DSFは本実験にメンバーとして参加し、実験の実作業を担いました。さらにDSFは、本実験で新たに考案あるいは改善した手順や記述方法をより実践的な知見として本ガイドに取り入れ、活動の集大成として本ガイドの最終版を本日公開します。

なお、DSFは所有する成果物の著作権を2012年6月にIPAに譲渡する予定であり、2012年6月末日に活動を終了しますが、参加各社において本取り組みの成果を生かし形式手法の普及に努めます。また、IPA は今回の実験成果を形式手法の現場普及を目指した教材に取り入れ、開発現場が形式手法を適切に活用できるよう普及を図ります。さらに本実験とは異なる観点を含めた形式手法の実証実験を継続して行い、形式手法を有効活用するための知識体系を整理していく予定です。

本実験と本ガイドについては、別紙をご参照ください。

添付資料

•  別紙（140KB）

注釈

注1 独立行政法人情報処理推進機構：

理事長 藤江 一正

注2 形式手法（フォーマルメソッド、Formal Methods）：

数理論理を基礎として、対象とするシステムやソフトウェアの機能・振る舞いについて正確な記述と系統的な検証を行う手法・技術の総称。対象を厳密に記述することにより、要求や設計の矛盾、抜け漏れ等の誤りに気付く。さらにツールを用いて検証することにより、要求や設計仕様の矛盾、抜け漏れ等の誤りを発見することができる。

注3 株式会社NTTデータ、富士通株式会社、日本電気株式会社、株式会社日立製作所、株式会社東芝、SCSK株式会社の6社および大学共同利用機関法人 情報・システム研究機構 国立情報学研究所：

株式会社NTTデータ（代表取締役社長：山下 徹）、富士通株式会社（代表取締役社長：山本 正已）、日本電気株式会社（代表取締役 執行役員社長：遠藤 信博）、株式会社日立製作所（代表執行役 執行役社長：中西 宏明）、株式会社東芝（取締役 代表執行役社長：佐々木 則夫）、SCSK株式会社（代表取締役社長：中井戸 信英）の6社と、大学共同利用機関法人 情報・システム研究機構 国立情報学研究所（所長：坂内 正夫）

注4 エンタプライズ系ソフトウェア：

企業活動を営むための業務システムや社会基盤を支える情報システムの機能を実現するソフトウェアのこと。

注5 指摘事項：

形式手法適用者が、設計書の機能仕様を形式手法で記述、検証したときに指摘した事項。

---