プロジェクトマネジャー：　黒川　利明　（株式会社ＣＳＫ　ＣＳＫフェロー）

１．プロジェクト全体の概要

本プロジェクトでは、ソフトウェア開発で最近最も重要な部分という認識が高まってきた上流工程の部分のうち、「要求」に対する支援のための各種方法論、ソフトウェアシステム、ソフトウェアツールなどの開発を目的とする。狙いは、特に、わが国において遅れていると言われる要求部分の技術者を育成するとともに、要求部分の品質を高めて、わが国のソフトウェアの品質向上と、わが国の産業の競争力強化にある。残念なことに、要求の重要性を認識しながらも、その研究開発が困難なために、応募数も7件という、他の分野に比べて少ないものだった。今回は、大学からの応募一件を採用できた。（もう一件の採用は、諸般の理由によりあきらめざるをえなかった。）これは、代数仕様における不動点定理を利用した自動検証支援を行うものであり、今後の発展が期待される。

２．プロジェクト採択時の評価（全体）

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

３．プロジェクト終了時の評価

「要求仕様の自動検証システムの開発」で作成されたシステムには、Crèmeという名前がつけられた。システム実装には、Common Lispが用いられた。ユーザ・インタフェースは、メディア系のシステムのようなマウスを使ってグラフィックに操作するものではなく、基本的には、コマンド入力の形式をとる。見映えは、したがって、余り良いものではない。

しかし、不動点帰納法を用いた補題の発見と、仕様の検証という当初の目標は無事に達成できた。証明構造の図　　

示は、利用者にとって有用なだけでなく、システム開発においても役立ったようだ。また、一般的にはなじみの薄

い、代数仕様に基づいたこのような検証システムに対する、丁寧な説明書が作成されており、今後のシステム移

植を含めた、拡張及び利用可能性が確保されているのは喜ばしい。