研究課題
我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、attackersの参入や新しい認証子の発行等のようなシステムのダイナミックな変化を捉える方法論を確立することが重要である。昨年度の準備研究の成果を踏まえて、protocol logicsの論理的分析を中心として、論理的検証の方法論の具体的応用を与えた。また、特に、認証プロトコルのagreement properties検証に関するprotocol logicの基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。
すべて 2006 2005
すべて 雑誌論文 (5件) 図書 (1件)
Mathematical Structure in Computer Science (近刊)
Algebra, Meaning, and Computation. A Festschrift in Honor of Prof. Joseph Goguen 近刊
Reasoning and Cognition, (Keio University Press) 近刊
Electronic Notes in Computer Science, Invited Paper of the 6th International Workshop on Rule-Based Programming (RULE'05) vol.147(1)
ページ: 73-92
