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

超越模型检验方法限制的动态实时系统逻辑验证方法

• 批准号: 15017278
• 负责人: 岡田 光弘
• 金额: $ 1.66万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2003
• 资助国家: 日本
• 起止时间: 2003 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15017278/
• 关键词: 論理的手法; 線形論理; 形式仕様; 形式検証; 実時間システム; 証明論

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

Linear logic is based on finite state theory, and the theory of time parallel system is studied. The logical proof theory of self is opposite, and the secondary characteristics are different. 1. Methodology of system logic and methodology of automatic verification of system security, classification, classification and classification problems. 2. The evolution and development of the system are unique to the analysis and analysis. The number of entries increases, the time constraints change, the time constraints change, and the logic of the entries change. 3. A part of the critical state is generated by the analysis of the development of the logical inference system. In addition, the theory and implementation of the system are based on the INRIA-LRI-LIX system. The basic part of the theory of the Japanese side (Okada) is based on the theory of the Japanese side (Okada) This is the first time I've ever seen such a thing. Okada-Jouannaud The research collaborator, Kobe Ota, made logical speech. In addition, the preparation for the application of this new methodology (especially, the preparation for the application of time constraint authentication, including the identification of time constraints) is carried out. The research on the logic of authentication and the logic of time constraint in communication is progressing.

项目成果

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

Mitsuhiro Okada：“线性逻辑和直觉逻辑”《国际哲学评论》（即将出版）。

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)

M.Okada、B.Pierce、A.Scedrov、H.Tokuda、A.Yonezawa：“软件安全，软件安全国际研讨会论文集，2002 年”Springer，热门话题系列。

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

M.Kanovitch、Mitsuhiro Okada、A.Scedrov：“轻线性逻辑的相位语义”理论计算机科学。

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)

H.Kushida，M.Okada：“经典逻辑和模态逻辑对应关系的证明理论研究”符号逻辑杂志。

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

冈田光宏：“矛盾是矛盾吗？”36・2（2004）。