１．担当ＰＭ

   黒川　利明　（株式会社CSK　CSKフェロー）

２．採択者氏名

３．プロジェクト管理組織

　 日本エンジェルズ・インベストメント株式会社

４．採択金額

　 9,000,000 円

５．テーマ名

　 要求仕様の自動検証システムの開発

６．関連Webサイト

　　なし

７．申請テーマ概要

　　信頼性の高いシステムを開発するためには，仕様を記述し検証することが有効である． しかしあまり広くは利用されていない．

その原因として
　・検証には多大な労力を必要とする.
　・検証にはシステム固有の知識の獲得を必要とする．
ことがあげられる．

本テーマの目標はシステム開発における仕様の検証を支援するソフトウェアツールを開発し， 信頼性の高いシステムを実現することにある．

具体的には，
　・システム開発の上流工程における仕様の検証を自動化する．
　・自動で生成された証明の構造を図示し，視覚的な理解を助ける．
　・検証結果よりシステムの重要な性質を明らかにする．
これらのことを行うことで，正しいシステムの開発を支援する．

８．採択理由

　要求仕様の検証は、要求周りの技術の中でも重要なものである。本提案は、この課題に対して不動点計算法を適用しようというものである。「自動化」支援によって、要求仕様の検証を技術として定着させようという取り組みを高く評価した。ただし、前提となる論理的な仕様の表現は、利用者が用意しないといけないと言うハードルは未だに残っており、この技術が直ちに一般に広く使えるものではない。