2007 Fiscal Year Annual Research Report
証明支援系とモデル検査器を効果的に利用できる環境と方法論
| Project/Area Number |
18500019
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 Japan Advanced Institute of Science and Technology, 情報科学研究科, 特任准教授 (30272991)
|
|---|
| Keywords | 有界モデル検査 / 定理証明 / 数学的帰納法 / 観測遷移システム / CafeOBJ / Maude / 反例 / 補題 |
|---|
| Research Abstract |
平成19年度は主に以下のことを行った。
1.有界モデル検査と数学的帰納法の組み合わせによる反例発見の実例への応用:提案方法の有効性を確認するため,ある性質を満たさないことがわかっている電子商取引プロトコルiKPへの適用を試みた。iKPは,多くの認証プロトコルより複雑で規模も大きいため,モデル検査だけでは反例を発見できないと予測した。しかし,反例が初期状態から浅い位置にあるため,予測に反し,有界モデル検査だけで反例を発見できた。
2.観測遷移システムのCafeOBJ仕様からMaude仕様への変換:観測遷移システムの遷移を書換え規則で素直に記述すると,各状態を表す項が大きくなる。記述方法を工夫することで,各状態を現す項を大きくならないようにした。
3.Mondex電子財布システムの検証:定理証明による検証において最も知的な作業の1つは,適切な補題を発見することである。補題が正しくなかったり,正しくても補題自身の証明が困難だったりすれば,検証を成功させることはできない。この検証では,補題を使用する前に,モデル検査により補題に反例がないことを確認することで,正しくない補題の使用を防ぐことを行った。検証中,一見正しいと思われた補題が,モデル検査により反例があることを発見でき,無駄な作業を防ぐことができた。
|
Research Products
(3 results)
