2007 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では9種類の図を用いてシステムの異なった側面を記述するが,従来の研究では単一の図を対象とした検証しかされておらず,それらを組み合わせて実装したときに発生する複雑な誤りは発見できなかった.
そこで本研究課題では,上記のような誤りを検出するため,複数のUML図を統合してモデル検査を行うための手法について研究開発を行った.特に,統合によるモデルの巨大化に伴って検証コストが指数的に増大することが予想されるため,有界モデル検査の適用とその効率化について研究を行った.
具体的には,有界モデル検査を適用するため,特定のUML図の組合せによって記述されたシステムの仕様記述から,統合されたモデルを求める手法を考案し,例題システムへの適用実験を通して有効性を示した.また適用実験のー環として,UML図によってモデル化されたWebナビゲーションの検証に対しても提案手法を適用した.さらに,有界モデル検査を複数UML図の検証に最適化するため,様々なアルゴリズムを適用して比較実験を行った.
その成果として,複数のUML図を統合してモデル化し,有界モデル検査による検証を行う枠組みの開発に成功した.さらに検証を効率化することで,大規模なソフトウェア開発に対して提案手法を適用するための見通しが得られた.
|
Research Products
(3 results)
