ニュース / News

ニュースリリース

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

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

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

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

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

1643

注目コンテンツ / SPECIAL