2004 Fiscal Year Annual Research Report
モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法
| Project/Area Number |
16016276
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Keywords | 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論 |
|---|
| Research Abstract |
1.我々の形式仕様・形式検証の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。又、このロジカル・リーズニングの基本として線形論理を用いることが有効であることを示してきた。形式仕様記述には線形論理が用いられ、仕様を満たすプロセスは線形論理証明で表示され、安全性等の自動検証のために必要とされる稠密時間概念の消去手続は線形論理証明の変換手続として実現された。このような線形論理を用いたロジカル・リーズニングが安全性自動検証などの一部の検証に有効であるのみならず、実時間システムの改良や修正等のより広い範囲の分析にも有効であることを示す目的で、実装計画を進めた。
2.我々の方法論をダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して応用した。現在までに試作した我々の線形論理自動検証系FATALISをダイナミックシステムの検証に適するように改良を進めた。
3.セキュリティプロトコルの安全性検証のためのProtocol Logicsの主要部分が一階述語論理上で実現できることを示した。又、tracesをベースとしたformal semanticsを与え、我々のprotocol logicのsemantic completenessを与えた。又、これを使って我々のprotocol logicの決定問題を肯定的に解いた。さらにこの完全性証明を用いて時間制約を含む具体的なprotocolの安全性証明や反例生成の方法論を開発中である。
|
