東京証券取引所の設計書を対象とした実験で形式手法の有効性を実証
～実験結果をもとにDSFが「形式手法活用ガイド」を完成～

独立行政法人情報処理推進機構（以下、IPA）^(注1)は、株式会社東京証券取引所で実際に運用しているシステムの設計書を対象にして、ディペンダブル・ソフトウェア・フォーラム（以下、DSF）の活動成果である形式手法活用ガイド（以下“本ガイド”）に従って、形式手法^(注2)適用実証実験（以下“本実験”）を2011年8月より行い、形式手法の有効性を実証しました。IPA は本実験の結果を報告書（以下“本書”）にまとめ、IPA公式Webサイト で公開します。

DSFは、障害を起こさないソフトウェア（ディペンダブル・ソフトウェア）を実現するために、形式手法のソフトウェア開発への導入を目指し2009年より活動してきましたが、本実験の結果を受けて本ガイドを改訂し、最終版をDSF公式Webサイト で公開します。

なおDSFには、株式会社ＮＴＴデータ、富士通株式会社、日本電気株式会社、株式会社日立製作所、株式会社東芝、SCSK株式会社の6社および大学共同利用機関法人 情報・システム研究機構 国立情報学研究所^（注3）が参加しています。

【概要】

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

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

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

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

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

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

（注1）独立行政法人情報処理推進機構　理事長　藤江　一正

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

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

（注4）エンタプライズ系ソフトウェア
企業活動を営むための業務システムや社会基盤を支える情報システムの機能を実現するソフトウェアのこと。

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

本件に関するお問い合わせ先

【報道関係のお問い合わせ先】	【その他のお問い合わせ先】
株式会社NTTデータ 広報部 平形・高橋 TEL ： 03-5546-8051	株式会社NTTデータ 技術開発本部 塚本・田端 TEL ： 050-5546-8779
富士通株式会社 パブリックリレーションズ本部 広報IR室 小川・遠藤 TEL ： 03-6252-2174	富士通株式会社 共通技術本部 銀林 TEL ： 03-6424-6276
日本電気株式会社 コーポレートコミュニケーション部 上田 TEL ： 03-3798-6511	日本電気株式会社 ソフトウェア生産革新部 岩崎 TEL ： 03-3798-8405
株式会社日立製作所 情報・通信システム社 広報部 菊池 TEL ： 03-5471-8900	株式会社日立製作所 情報・通信システム社 プロジェクトマネジメント統括推進本部 福地 TEL ： 03-5471-2942
株式会社東芝 広報室広報担当 吉村 TEL ： 03-3457-2100	株式会社東芝 ソフトウェア技術センター 長谷川 TEL ： 044-549-2458
SCSK株式会社 広報部 秦・神谷 TEL ： 03-5166-1150	SCSK株式会社 ソリューション・機能事業部門 開発ソリューション事業本部 開発部 植木 TEL ： 03-5290-3872
大学共同利用機関法人 情報・システム研究機構 国立情報学研究所 総務部企画課 広報チーム 坂内 TEL ： 03-4212-2164 E-mail ： kouhou@nii.ac.jp	大学共同利用機関法人 情報・システム研究機構 国立情報学研究所 アーキテクチャ科学研究系 中島 TEL ： 03-4212-2507
独立行政法人情報処理推進機構 戦略企画部 広報グループ 横山・白石 TEL ： 03-5978-7503	独立行政法人情報処理推進機構 技術本部 ソフトウェア・エンジニアリング・センター 向山 TEL ： 03-5978-7543

※掲載されている製品名、会社名、サービス名はすべて各社の商標または登録商標です。