6社とDSF、形式手法適用実証実験をIPA SEC主催で開始

　NTTデータ、富士通、日本電気、日立製作所、東芝、CSKの6社と、大学共同利用機関法人　情報・システム研究機構　国立情報学研究所が参加するディペンダブル・ソフトウェア・フォーラム(Dependable　Software　Forum、略称名はDSF)は、独立行政法人　情報処理推進機構　ソフトウェア・エンジニアリング・センター(以下、IPA　SEC)のワーキンググループに参加し、東京証券取引所のエンタプライズ系ソフトウェアを対象とした形式手法の有効性実証実験を実施する。

　形式手法とは、品質の高いソフトウェアを効率よく開発するために、数学を基盤とした矛盾のない仕様書を書いて、それが正しいかどうかを検証する手法のこと。そのため、高信頼・高品質が求められる自動車や家電等のハードウェアに組み込まれる組込み系ソフトウェアを中心に、形式手法を適用した開発を推奨する動きがあり、形式手法に注目が集まっている。しかし、エンタプライズ系ソフトウェアについては適用事例が少なく、その効果も一般に公開されていない。そこでDSFはエンタプライズ系ソフトウェアに形式手法を適用するための事例およびノウハウの収集を行っていくという。

　ソフトウェアを開発するプロジェクトにとって、形式手法の利活用は作業期間や作業コストに影響する。よって事前に発注者(ユーザ)と受注者(ベンダ)が合意するために、利活用の可否を判断する情報(形式手法によって除去できる欠陥の数や作業人月など)が必要となるという。そこで同実験では上記情報を収集し、実験実施後に実験報告書としてIPA　SECから公開する。

　なお同実験では、DSFが作成した形式手法活用ガイドを活用。同ガイドはエンタプライズ系ソフトウェアを対象とした形式手法の適用手順や典型的な形式記述の例をまとめたもの。同実験と並行してDSFメンバで本ガイドの社内評価の開始準備が整ったことにより、DSF社内外の実利用で評価される品質に達したものとして、DSF公式ホームページで正式リリースするという。