東京証券取引所とDSF成果を活用した形式手法適用実証実験をIPA SEC主催で開始 ～DSFが「形式手法活用ガイド」を正式リリース～

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

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

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

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

またDSFは本実験を通じて得られた知見を本ガイドにフィードバックし、2012年3月に改訂版として公開します。

経済産業省は「新世代情報セキュリティ研究開発事業」により、情報家電などの組込みソフトウェアに対する形式手法適用のケーススタディを収集し、普及促進のためガイダンスを作成しました。また同省北海道経済産業局は、北海道および中部地区に拠点を持つ中小ソフトウェア企業を中心に組込みソフトウェアを対象とした現場普及活動を行っています。

さらにIPA SECは本実験以外にも、形式手法を利用できる人材の育成や過去事例の整理を中心とした形式手法の普及活動を行っています。

このように形式手法に対する関心が高まる中で、DSFは社会における重要性が飛躍的に高まるエンタプライズ系ソフトウェアを対象とした初の形式手法活用ガイドを作成しました。

また公的機関であるIPA SECや発注者の立場である株式会社東京証券取引所と連携して本実験を実施し、結果を実験報告書としてまとめます。

本実験はIPA SECのワーキンググループで実施し、メンバとしてDSFおよび株式会社東京証券取引所、さらに有識者が参加します。具体的には、エンタプライズ系かつ高信頼が求められるシステムを多く保有する株式会社東京証券取引所で現在稼働中のソフトウェアの設計書を対象に、形式手法活用ガイドの手順に従って設計書の不整合や曖昧さなど設計書としての欠陥の除去を実施します。また株式会社東京証券取引所の評価を得た上で、開発中に発見した欠陥との比較や除去した欠陥の数や種類、作業人月などを実験報告書にまとめます。これにより報告内容に発注者の見解を取り入れることができるため、報告内容の信頼性を向上することができます。さらに有識者から実験データの客観的な分析を加えることで、報告内容の信頼性および汎用性を高めます。

本ガイドは、形式手法による設計書の欠陥除去手段の確立を目的とし、受注者（開発プロジェクト）向けにその手順と参考となる形式記述の例をまとめたものです。以下三つのラインアップについて個別に説明します。

DSFは、エンタプライズ系ソフトウェアの信頼性・安全性向上のため、現場への形式手法導入課題を解決する活動として2009年12月22日に形式手法適用評価ワーキンググループ（以下、"FMAWG"）を設立しました。

FMAWGは形式手法の記述実験で得られた知見をベースに検討し、成果物第一弾として2010年11月に形式手法活用ガイドのドラフト版を公開しました。その後もさらに活動を継続し、代表的な三つの形式手法（VDM++、SPIN、Event-B）について形式手法活用ガイドの充実を図りました。本実験と並行してDSFメンバで本ガイドの社内評価の開始準備が整ったことにより、DSF社内外の実利用で評価いただける品質に達したものとして、今回正式版としてリリースしました。

DSFは本実験に参加、形式手法利活用の可否を判断するために必要な情報（形式手法によって除去できる欠陥の数や作業人月など）を収集し、実験報告書としてIPA SECから公開します。また同時に、本実験で本ガイドの手順に従った欠陥除去を実施した経験から本ガイドの課題抽出および対策を実施し、2012年3月に改訂版として公開します。