2008 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 |
平成20年度は主に以下のことを行った。
1. 定理証明向き仕様からモデル検査向き仕様への変換の形式化と正当性の証明:定理証明向きの観測遷移システムの振舞仕様を、モデル検査向きの書換え論理仕様に変換する場合、遷移等に現れるパラメータをそのままにすると、有界の書換え論理仕様では表現できない振舞仕様があることがわかった。有界の書換え論理仕様で表現できる方法を考案した。提案手法は、パラメータを具現化することである。提案した変換方法を形式化し、変換の正当性を証明した。変換の正当性とは、変換後の仕様で反例が見つかった場合、それは変換前の仕様においても反例である、ということである。
2. 実用的な変換方法:セキュリティプロトコルの振舞仕様を書換え論理仕様に変換する場合、状態を表す項が巨大になる傾向がある。これは、書換え規則に現れる遷移のパラメータの表現方法に問題があることがわかった。パラメータの提供する情報と等価なものを項で表現することで、パラメータを除去できることがわかり、これにより状態を表す項が巨大にならないような変換方法を提案した。
3. 変換器の実装:これまでは、変換器はJavaで実装していた。Java等の通常のプログラミング言語で実装する場合、構文解析器等も自前で用意する必要があった。一方、Maudeのメタプログラミング機能を用いると、構文解析器等を自前で用紙する必要はなく、部品の再利用性も向上することがわかってきた。そこで、Maudeを用いて変換器を実装しなおした。複数の変換規則を簡便に埋め込むことができることがわかり、より拡張性の高い実装を得ることができた。
|
