富士通ら、東京証券取引所の設計書で形式手法の有効性を実証実験

IPAは4月20日、東京証券取引所で運用しているシステムの設計書を対象に、ディペンダブル・ソフトウェア・フォーラム(以下、DSF)の活動成果である形式手法活用ガイドに従って、形式手法適用実証実験を2011年8月より行い、形式手法の有効性を実証したと発表した。

IPAは同実験の結果を報告書にまとめ、公式Webサイトで公開する。

DSF(Dependable Software Forum)は、障害を起こさないソフトウェアを実現するために、実践的かつ系統的・論理的な設計技術を確立させる研究開発を行い、ソフトウェアに起因するシステム障害の低減を目指し、2009年より活動してきた。NTTデータ、富士通、日本電気、日立製作所、東芝、SCSKの6社および大学共同利用機関法人 情報・システム研究機構 国立情報学研究所がDSFに参加している。

エンタプライズ系ソフトウェアの分野では開発現場への形式手法導入を支援するガイドがなかったことから、DSFは形式手法の適用手順や典型的な形式記述の例をまとめたガイドを作成し、2011年7月21日に公開した。今回の実験結果を受けてガイドを改訂し、最終版をDSF公式Webサイトで公開する。

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

同実証実験において、東京証券取引所で実際に運用しているシステムのレビュー実施済みの設計書に形式手法を適用したところ、設計書レビューでは発見されなかった指摘事項を発見した。東京証券取引所が設計書を修正すべきであると評価した指摘事項のうち半数以上は、従来では実装やテストといった設計工程以降で発見されていたものだったが、今回の検査では、設計工程で発見できた。

これより、IPAでは設計工程以降に発生する作業の手戻りが削減できる可能性を示すことができたとしている。