富士通株式会社
日本電気株式会社
株式会社日立製作所
株式会社東芝
SCSK株式会社
大学共同利用機関法人 情報・システム研究機構 国立情報学研究所
独立行政法人情報処理推進機構
東京証券取引所の設計書を対象とした実験で形式手法の有効性を実証
~実験結果をもとにDSFが「形式手法活用ガイド」を完成~
-
独立行政法人情報処理推進機構(以下、IPA)(注1)は、株式会社東京証券取引所で実際に運用しているシステムの設計書を対象にして、ディペンダブル・ソフトウェア・フォーラム(以下、DSF)の活動成果である形式手法活用ガイド(以下“本ガイド”)に従って、形式手法(注2)適用実証実験(以下“本実験”)を2011年8月より行い、形式手法の有効性を実証しました。IPA は本実験の結果を報告書(以下“本書”)にまとめ、IPA公式Webサイト で公開します。
DSFは、障害を起こさないソフトウェア(ディペンダブル・ソフトウェア)を実現するために、形式手法のソフトウェア開発への導入を目指し2009年より活動してきましたが、本実験の結果を受けて本ガイドを改訂し、最終版をDSF公式Webサイト で公開します。
なおDSFには、株式会社NTTデータ、富士通株式会社、日本電気株式会社、株式会社日立製作所、株式会社東芝、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)株式会社NTTデータ(代表取締役社長 : 山下 徹)、富士通株式会社(代表取締役社長 : 山本 正已)、日本電気株式会社(代表取締役 執行役員社長 : 遠藤 信博)、株式会社日立製作所(代表執行役 執行役社長 : 中西 宏明)、株式会社東芝(取締役 代表執行役社長 : 佐々木 則夫)、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-2458SCSK株式会社
広報部 秦・神谷
TEL : 03-5166-1150SCSK株式会社
ソリューション・機能事業部門
開発ソリューション事業本部 開発部 植木
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 -
※掲載されている製品名、会社名、サービス名はすべて各社の商標または登録商標です。