| 研究課題/領域番号 |
16016276
|
|---|
| 研究種目 |
特定領域研究
|
| 配分区分 | 補助金 |
|---|
| 審査区分 |
理工系
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究期間 (年度) |
2005 – 2006
|
| 研究課題ステータス |
完了 (2005年度)
|
| 配分額 *注記 |
5,500千円 (直接経費: 5,500千円)
2005年度: 2,900千円 (直接経費: 2,900千円)
2004年度: 2,600千円 (直接経費: 2,600千円)
|
|---|
| キーワード | 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論 |
|---|
| 研究概要 |
我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。
我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。
論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、attackersの参入や新しい認証子の発行等のようなシステムのダイナミックな変化を捉える方法論を確立することが重要である。昨年度の準備研究の成果を踏まえて、protocol logicsの論理的分析を中心として、論理的検証の方法論の具体的応用を与えた。
また、特に、認証プロトコルのagreement properties検証に関するprotocol logicの基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。
|
