课题基金 / 基金详情

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

モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法
超越模型检验方法限制的动态实时系统逻辑验证方法
批准号：
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の基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。
期刊论文(26)
专著(0)
科研奖励(0)
会议论文
Inferences on Honesty in Compositional Logic for Security Analysis
证券分析组合逻辑中诚实性的推论
DOI： --
发表时间： 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 测试”的开发
DOI： --
发表时间： 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
基本协议逻辑的完整性和反例生成
DOI： --
发表时间： 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
演绎推理和抑制机制的认知神经科学：关于信念偏差效应
DOI： --
发表时间： 2006
期刊： Reasoning and Cognition, (Keio University Press) 近刊
影响因子： --
作者： [Takeo Tsujii, Mitsuhiro Okada, Shigeru Watanabe]
通讯作者： Shigeru Watanabe
共 12 条
    論証・証明の哲学の深化に向けた学際的「論理の哲学」研究
    • 批准号：
      23K20416
    • 项目类别：
      Grant-in-Aid for Scientific Research (B)
    • 资助金额：
      $3.24万
    • 财政年份：
      2024
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    On information presentation methods for easier decison making: Studies on multi-attribute decision making
    • 批准号：
      21K18339
    • 项目类别：
      Grant-in-Aid for Challenging Research (Exploratory)
    • 资助金额：
      $4.08万
    • 财政年份：
      2021
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    Interdisciplinary studies on philosophy of logic: Toward the development of philosophy of proof and demonstration
    • 批准号：
      21H00467
    • 项目类别：
      Grant-in-Aid for Scientific Research (B)
    • 资助金额：
      $8.49万
    • 财政年份：
      2021
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    Study on "Disagreement" in logic
    • 批准号：
      19KK0006
    • 项目类别：
      Fund for the Promotion of Joint International Research (Fostering Joint International Research (B))
    • 资助金额：
      $7.49万
    • 财政年份：
      2019
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    海外基金