| 研究概要 |
大規模なソフトウェアの開発においては, 設計段階で混入した誤りや不具合による手戻りが, 開発プロセス全体のコストに与える影響が非常に大きくなる. これを防ぐためにUMLを始めとした形式的な仕様記法がソフトウェアの設計に広く用いられている. あらかじめ定め照れた記法に従って設計を行うことにより, 設計の曖昧性や開発者間の誤解を避けることができる. しかしながら, ソフトウェアが設計者の意図した通りの動作を行うか, といった動的な側面における正しさについては形式仕様記法では保証できない. そこで本研究課題では, 動的性質の検証手法である有界モデル検査を用いたUML設計検証手法について研究開発を行っている. ここで提案する設計検証手法はソフトウェアの各モジュールの動作とモジュール間のメッセージ通信に関する設計に注目しており, 各モジュールが与えられたメッセージ通信仕様を満たすか有界モデル検査により検証するものである.
まず, モジュールの動作並びにモジュール間のメッセージ通信を記述するUML設計群から有界モデル検査のためのモデルを抽出する手法について研究開発を行った. 提案手法では, 各UML設計で記述された動的振る舞いを論理式表現し, それらを組み合わせることで有界モデル検査による検証を実現している. さらに, 提案する検証系の実装のため, 与えられたUML設計群から論理式表現を自動生成するツールを開発した. また本研究課題では適用実験の-環として, Webページのナビゲーション構造の検証についても研究開発を行い, UMLの状態マシン図によりモデル化されたナビゲーション構造をモデル検査により検証する手法について研究開発を行った.
本年度の成果として, UML設計群として与えられたモジュールの動作並びにモジュール間のメッセージ通信が互いに矛盾なく記述されているかを有界モデル検査により検証する枠組みを実現するとともに, 自動検証ツールについて実装の一部を完了した。また, 適用実験として, Webナビゲーション構造の設計に対して提案法による検証を行い, 有効性を確認した.
|
