2008 Fiscal Year Annual Research Report
| Project/Area Number |
20650003
|
|---|
| Research Category |
Grant-in-Aid for Exploratory Research
|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 University of Tsukuba, 大学院・システム情報工学研究科, 准教授 (10195000)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
木下 佳樹 (独)産業技術総合研究所, システム検証研究センター, センター長 (60356889)
西澤 弘毅 鳥取環境大学, 環境情報学部, 講師 (60455433)
|
|---|
| Keywords | 多値モデル検査 / システム検証 / モデル化 / 状態遷移系 / 安全性検証 / 抽象化 |
|---|
| Research Abstract |
本研究は、モデル検査法を用いたシステム設計検証において、しばしば問題となる「モデル化の誤り(モデリング・エラー)」を発見する手法の研究を行うものである。モデル化に誤りがあるときは、仮にモデル検査器が「検証成功」という結果を出力しても、システム設計が正しいことは保証されないため、これは深刻な問題である。
本研究の中心となるアイディアは、「検証成功」という結果になったときに、モデルの一部を意図的に変更し、「検証失敗」となる限界のモデルを探索することにより、モデリング・エラーの原因を探るというものである。本年度の研究では、まず、モデリング・エラーの事例研究を行い、実際のシステムの設計検証の場面において、どのような誤りがあり得るかについて事例検討を行った。次に、限界モデルを効率的に探索する際に鍵となる技術である多値モデル検査法の性能向上に取り組んだ。その結果、有界モデル検査法を多値モデルに拡張した手法において、探索効率を向上させる符号化法を発見し、実装を行うことができた。この方法では、128値程度の多値モデルに対するモデル検査においても、2値の場合のモデル検査の数倍程度の時間で実行することができるがわかった。これにより、本研究の目的であるモデリング・エラー発見システムの構築にある程度の見通しが立った。
|
