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

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

• 批准号: 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の基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。

我们研究的框架是使用逻辑推理和演绎方法，将逻辑推理纳入形式化规范和形式化验证中，用于构建实时系统（例如传统的模型检查方法），它具有最大的特点（不同于自动机理论分析） ）。我们已经证明，我们的方法对于特定于允许动态变化的进化和发展实时系统的验证和分析是有效的。我们还得到了神户大学田村实验室小组的合作，以逻辑编程语言实现我们的理论。我们还整合了以前的理论和实践研究。我们还将逻辑形式验证的方法应用于认证协议的安全验证。在身份验证协议的逻辑验证中，重要的是建立一种捕获系统动态变化的方法，例如攻击者的进入或新身份验证器的发布。在去年前期研究成果的基础上，我们给出了逻辑验证方法论的具体应用，重点是协议逻辑的逻辑分析。特别是，我们用一阶谓词逻辑重构了与认证协议的协议属性验证相关的协议逻辑的基本部分，并给出了其完备性定理和反例生成系统。我们还创建了一个反例生成系统的原型实现来应用该理论。我们还对验证认证协议安全性的实时分析方法进行了研究。

项目成果

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