2003 Fiscal Year Annual Research Report

モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

Research Project

Project/Area Number	15017278
Research Institution	Keio University
Principal Investigator	岡田光弘慶應義塾大学, 文学部, 教授 (30224025)
Keywords	論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論
Research Abstract	線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する我々のこれまでの成果をもとにして、論理的手法による実時間システム検証の理論の研究を進めた。我々の論理的検証理論は、次のような特徴を持つものとなる。 1.体系的で論理的な形式仕様の方法論及び、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論である。 2.ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性である。エージェントの数が増加したり時間制約が動的に変化したりするような、ダイナミックで現実的な実時間システムに応用できる論理的検証ツールが実現できる。 3.一部に危険な状態が生じ得ることが分かっている実時間システムのなかで、システムの仕様にどのような手直しをすれば安全になるかを我々の論理的推論体系を用いて分析するツールの開発である。又、我々の理論の実装にあたっては、フランス側INRIA-LRI-LIXグループとともに論理的形式仕様・検証言語Coq-System上で行なった実装試作を基盤として用いた。実装試作は日本側(岡田)が我々の理論的成果に基づいて検証手続の基本部分の具体的アルゴリズムを理論から抽出して進められた。この実装作業はCoq-グループの2人の大学院生により進められた。岡田-Jouannaudが共同指導教員となりこの作業を進めている。研究協力者神戸大田村グループと論理型言語を使った実装も行なった。又、この新しい方法論の実践的な応用を目的にした研究(特に、実践的な実時間制約や時刻認証を含んだ枠組での認証プロトコルのセキュリティ分析など)の準備を行なった。このために認証プロトコルの論理的検証理論や通信プロトコルの時間制約の論理的分析についての研究を進めた。

Research Products

(7 results)

All Other

All Publications (7 results)

[Publications] H.Kushida, M.Okada: "A proof-theoretic study of the correspondence of classical logic and modal logic"Journal of Symbolic Logic. 68・4. 1403-1414 (2003)
[Publications] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)
[Publications] K.Hasebe, J-P.Jouannaud, A.Kremer, M.Okada, R.Zumkeller: "Formal Verification of Dynamic Real-Time State-Transition Systems Using Linear Logic"日本ソフトウェア科学会第20回全国大会予稿集. (2003)
[Publications] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)
[Publications] M.Kanovitch, Mitsuhiro Okada, A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. 294. 525-549 (2003)
[Publications] M.Nagayama, Mitsuhiro Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. 294. 551-573 (2003)
[Publications] M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security, proceedings of the International Symposium on Software Security, 2002"Springer, Hot-topic Series. (2003)

2003 Fiscal Year Annual Research Report

モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

Principal Investigator

岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)

Research Products

[Publications] H.Kushida, M.Okada: "A proof-theoretic study of the correspondence of classical logic and modal logic"Journal of Symbolic Logic. 68・4. 1403-1414 (2003)

[Publications] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)

[Publications] K.Hasebe, J-P.Jouannaud, A.Kremer, M.Okada, R.Zumkeller: "Formal Verification of Dynamic Real-Time State-Transition Systems Using Linear Logic"日本ソフトウェア科学会第20回全国大会予稿集. (2003)

[Publications] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)

[Publications] M.Kanovitch, Mitsuhiro Okada, A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. 294. 525-549 (2003)

[Publications] M.Nagayama, Mitsuhiro Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. 294. 551-573 (2003)

[Publications] M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security, proceedings of the International Symposium on Software Security, 2002"Springer, Hot-topic Series. (2003)

岡田光弘慶應義塾大学, 文学部, 教授 (30224025)