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

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

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

我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、attackersの参入や新しい認証子の発行等のようなシステムのダイナミックな変化を捉える方法論を確立することが重要である。昨年度の準備研究の成果を踏まえて、protocol logicsの論理的分析を中心として、論理的検証の方法論の具体的応用を与えた。また、特に、認証プロトコルのagreement properties検証に関するprotocol logicの基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。

In this paper, we study the deduction of group logic, the method of deduction, the method of time series construction, the method of formal proof, the method of system analysis and the method of theory analysis. Our methodology is based on the evolution, development, and analysis of the characteristics of the system. Tamura Laboratory, Kobe University, Japan The research of theory and the research of equipment are integrated. The formal verification methodology of logic is used to verify the safety of the system. It is important to establish a methodology for the verification of the logic of authentication protocols, the participation of attackers, and the development of new authenticators. The results of the preparatory study of the past year have been discussed in detail. The logical analysis of protocol logics and the specific application of logic verification methodology have been discussed in detail. The basic part of protocol logic is logically reconstructed, the completeness theorem and the counterexample generation system are logically reconstructed. The theory of the use of anti-example generation system and try to implement Research on Time Analysis Methods for Certification of Safety

项目成果

Inferences on Honesty in Compositional Logic for Security Analysis

证券分析组合逻辑中诚实性的推论

• 发表时间: 2004
• 期刊: Software Security-Theories and Systems Lecture Notes in Computer Science(Springer-Verlag) 3233
• 作者: Koji Hasebe;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada

A Crossroad of logic, psychology and behavioral genetics : Development of "BAROCO-test" in Keio Twin-Baroco Project

逻辑、心理学和行为遗传学的十字路口：Keio Twin-Baroco 项目中“BAROCO 测试”的开发

• 发表时间: 2006
• 期刊: Reasoning and Cognition, (Keio University Press) 近刊
• 作者: J.Ando;C.Shikishima;Y.Sugimoto;R.Takemura;P.Grialou;K.Hiraishi;M.Okada
• 通讯作者: M.Okada

Completeness and Counter-Example Generations of a Basic Protocol Logic

基本协议逻辑的完整性和反例生成

• 发表时间: 2005
• 期刊: Proceedings of the 6^<th> International Workshop on Rule-Based Programming, Electronic Notes in Theo.Comp.Sci. (to appear)
• 作者: Koji Hasebe;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada

Cognitive Neuroscience for Deductive Reasoning and Inhibitory Mechanism : On the Belief-Bias Effect

演绎推理和抑制机制的认知神经科学：关于信念偏差效应

• 发表时间: 2006
• 期刊: Reasoning and Cognition, (Keio University Press) 近刊
• 作者: Takeo Tsujii;Mitsuhiro Okada;Shigeru Watanabe
• 通讯作者: Shigeru Watanabe

Linear Logic and Intuitionistic Logic

线性逻辑和直觉逻辑

• 发表时间: 2005
• 期刊: La revue internationale de philosophie No.230
• 作者: K.Hasebe;M.Okada;Mitsuhiro Okada
• 通讯作者: Mitsuhiro Okada