2006 Fiscal Year Annual Research Report
証明支援系とモデル検査器を効果的に利用できる環境と方法論
| Project/Area Number |
18500019
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 特任助教授 (30272991)
|
|---|
| Keywords | 有界モデル検査 / 数学的帰納法 / 定理証明 / CafeOBJ / Maude / IGF / 変換器 / 補題発見 |
|---|
| Research Abstract |
平成18年度は主に以下のことを行った。
(1)有界モデル検査(Bounded Model Checking)と数学的帰納法(mathematical induduction)の組み合わせによる反例発見:有界モデル検査は,反例発見能力に優れており,ハードウェア等の産業界においては日常業務で使われている。しかし,状態空間爆発のため,初期状態から深い位置にある反例を発見することはできない.本研究では,反例発見を目的に状態空間爆発を緩和するため,数学的帰納法と有界モデル検査を組み合わせる方法を提案した.性質p1の反例が深さd+1にあるとき,p1を帰納法で証明するときに得られる補題の1つp2に必ず深さdに反例があるものがある.この事実を用いて,p1の代わりにp2に対して有界モデル検査を行うことができる.これにより状態空間爆発を緩和できると期待する.有界モデル検査と数学的気方法の組み合わせによる反例発見法を,IGF(Induction-Guided Falsification)と呼ぶ.有界モデル検査器としてMaudeを,数学的帰納法を支援する証明支援系としてCafeOBJを用いる.
(2)IGFの(半)自動化に関する考察:定理証明向きの状態機械(観測遷移システム)のCafeOBJ仕様から,モデル検査向きのMaude仕様への自動変換器,および数学的帰納法を適用して得られる補題を自動で検査する補題発見器が,IGFの(半)自動化には不可欠であることがわかった。
|
Research Products
(5 results)
