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

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

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

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

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

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

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

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

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

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