形式手法でソフトウェア設計時の修正指摘が可能に、IPAらが活動成果を報告

障害を起こさないソフトウェア「ディペンダブルソフトウェア」の実現に向け、IPAやITベンダーらが参加する組織が、東証のシステム設計書で形式手法を用いた効果を実証した。

[ITmedia]

　情報処理推進機構（IPA）や国立情報学研究所、ITベンダー6社が参加する「ディペンダブル・ソフトウェア・フォーラム（DSF）」は4月20日、障害を起こさないソフトウェア「ディペンダブルソフトウェア」の実現に向けた実証実験の成果報告書を発表した。

　この実験はソフトウェアに起因するシステム障害の低減を目的に、形式手法を使ってソフトウェア設計段階での修正指摘が可能かなどを検証したもの。DSFでは2011年8月から、東京証券取引所で実際に運用されているシステムのレビュー済みの設計書、のべ716ページを対象に形式手法を適用した場合の効果について調べた。

　その結果、設計作業終了後の設計書では55件の指摘事項を抽出。22件については東証が修正を指摘したもので、うち13件は設計作業後の実装やテストなどの工程で発見されたものであることが分かった。形式手法を用いれば、実際には設計後の工程で見つかった修正指摘を、設計時に発見できる効果が認められた。事前に修正部分を指摘できれば、設計後に行われる修正作業を大幅に削減できるとしている。

　DSFは実証実験の成果を反映させた形式手法活用ガイドの改訂版を公開。参加企業のNTTデータ、富士通、NEC、日立製作所、東芝、SCSKでは形式手法の普及を進め、IPAは人材育成などの場に役立てていくという。