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