１．担当ＰＭ

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

２．採択者氏名

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

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

４．委託金支払額

　 9,000,000 円

５．テーマ名

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

６．関連Webサイト

　　なし

７．テーマ概要

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

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

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

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

８．採択理由

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

９．開発目標

要求仕様の検証を支援するシステムの開発が、目標である。検証は、代数仕様で記述された要求仕様を、項書き換えエンジンを用いて実行することによって行われる。この際に、適切な補題を自動発見することによって、利用者側での試行錯誤の労力を軽減する。

１０．進捗概要

進捗を月ごとにまとめると次のようになる。

12月 不動点帰納法の設計

1月  データフロー・制御フローによる設計

2月  仕様記述言語とユーザ・インタフェースの設計

3月  サブプロセス Maude の出力修正

4月  Maude用のlisp側のインタフェース・場合わけの実装

5月  事前条件計算・不動点帰納法の実装

6月  Implier・Simplifierの実装

7月  補題発見器・証明図の生成機能の実装

8月  成果報告会、ドキュメント作成

この間、1月、3月、5月にサポート組織を含めて顔を突き合わせての、打ち合わせを行った。

　開発者がプロジェクト開始時に考えていたよりも、作業は遅れたのだが、PMとしては、この進捗は、順調なほうだと思う。

１１．成果

作成されたCrèmeシステムは、次のような構成になっている。

このシステムを用いて、利用者は、代数仕様の検証を、行うことができる。そのときに、補題発見器や証明図生成器を使うことによって、検証作業が容易になっている。

１２．プロジェクト評価

システム実装には、Common Lispが用いられた。ユーザ・インタフェースは、メディア系のシステムのようなマウスを使ってグラフィックに操作するものではなく、基本的には、コマンド入力の形式をとる。見映えは、したがって、余り良いものではない。

しかし、不動点帰納法を用いた補題の発見と、仕様の検証という当初の目標は無事に達成できた。証明構造の図示は、利用者にとって有用なだけでなく、システム開発においても役立ったようだ。また、一般的にはなじみの薄い、代数仕様に基づいたこのような検証システムに対する、丁寧な説明書が作成されており、今後のシステム移植を含めた、拡張及び利用可能性が確保されているのは喜ばしい。

東北大学　外山教授，産業技術総合研究所　大崎システム検証研究センター長とから,専門家としての講評もいただいた。現時点での技術達成は評価されているが、実用化のためには、まだ多くの課題も残っていることが指摘された。

１３．今後の課題

プロジェクト採択時の評価で述べたように、この技術が一般に広く活用されるためには、システムのモデル化支援をどうするか、代数仕様の生成をどうするかなど、課題は多い。代数仕様を含めた形式的なモデルの研究において、日本が必ずしも諸外国に大きく遅れているわけではないが、その実用化に向けた地道な取り組みが着実に行われていると言える状況にはない。

　しかしながら、最近は、モデルチェッカーの実用化への取り組みが積極的に行われるようになってきており、ソフトウェアの品質確保に向けて、形式手法を現場で使えるようにしようという取り組みは、VDMなども含め、民間でも各種行われるようになって来た。

　開発者は、今後理論的にもっと研究を続けたいと言っていたが、理論面・実践面を含めて、このような手法の開発を継続して、現場で使えるようにしていければよいと思う。