本研究課題では,動的性質の検証手法であるモデル検査を用いたUML設計群の検証手法について研究開発を行った.本研究では特に,ソフトウェアの各モジュールの動作とモジュール間のメッセージ通信に関する設計の整合性に注目しており,各モジュールが与えられたメッセージ通信仕様を満たすか有界モデル検査により検証するものである.また,UML設計群を一つのモデルに統合することによるモデルの巨大化に伴い,検証コストが指数的に増大することが予想されるため,有界モデル検査の適用とその効率化についても研究を行っている.
この目的を達成するため,まず,モジュールの動作並びにモジュール間のメッセージ通信を記述するUML設計群から有界モデル検査のためのモデルを抽出する手法について研究開発を行った.各UML設計で記述された動的振る舞いを論理式表現し,それらを組み合わせることで有界モデル検査による検証を実現する.次に,有界モデル検査をUML設計群の検証に最適化するため,状態空間の探索アルゴリズムの比較実験を行った.また,適用実験の一環として,Webページのナビゲーション構造の検証についても研究開発を行い,UMLの状態マシン図によりモデル化されたナビゲーション構造をモデル検査により検証する手法について研究開発を行った.最後に,提案する検証系を計算機上に実装するため,与えられたUML設計群から論理式表現を自動生成するツールを開発した.
その成果として,UML設計群として与えられたモジュールの動作並びにモジュール間のメッセージ通信が互いに矛盾なく記述されているかを有界モデル検査により検証する枠組みを実現するとともに,自動検証ツールについて実装の一部を完了した.また,適用実験として,Webナビゲーション構造の設計に対して提案法による検証を行い,有効性を確認した.