|
この研究では、実際のソフトウェアシステム開発に対して有効な検証方法を確立することを目指し、形式的仕様記述手法SOFL(Structured Object-oriented Formal Language)を基に形式的仕様の厳密的なレビュー技術かつテスト技術を確立し、更に、それらの技術の支援ツールの原型を開発した。厳密的なレビュー技術に関しては、伝統的な経験によりレビュー仕方を改善して、仕様記述言語の形式的意味を基づいて厳密的なレビュールールを確立した。この技術で形式仕様を検証するためには、まず、検証すべき条件を仕様書から導出する。次に、この条件をレビューするために、構造的なfault treeを構築し、そして、このtreeによってレビューを行い、その結果を分析する。今回のプロジェクトでは、検証すべき条件らを定義し、それらの条件を導出する方法を検討し、更に、fault treeの構築方法についても研究したが、未解決の問題点は、それらの検証条件からfault treeを自動的に構築する方法である。また、レビュー者が仕様をレビューすることをどのように支援すればいいということも解明してない。仕様テスト技術については、いくつかの課題を研究した。第一、実行不可能な形式的使用のテストするために、一般的な戦略(strategy)を解明した。プログラムのテストと違い、仕様をテストするためには、操作の入力と出力とともにテストケースを生成しなければならないことを明らかにした。第二、テストケース生成の様々な基準を定義した。第三、このテスト手法を用いて、既存のSOFL仕様をテストし、仕様テストの有効性を調べた。第四、仕様テストを支援するツールの原型を開発した。この原型は、将来より上質な支援ツールを開発に対して有意義な参考になると思う。また、形式的仕様を基づいてプログラムをテストする方法も研究し、その方法の有効性を調べた。伝統的なfunctionalテスト方法と比べて、形式的仕様によりプログラムテストの方が、全ての情況を考えることができるので、faultの発見効率が高いということを明らかにした。
|
