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

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

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

論理的手法による実時間システム検証の理論を情報学的観点から完成させることを本研究課題の目的としている。又この理論の実装に関して現れる情報学的問題を研究してきた。次のような特徴を持つ論理的検証系の理論を構築してきた。その第1は、実時間システム全体の設計に伴う、体系的で論理的な形式仕様の方法論および、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論の開発である。これまでに得られた我々の論理的検証系に対するPSPACE決定性定理を応用してこの方法論を開発してきた。その第2は、ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性の検討である。エージェントの数が増加したり、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールの方法論の開発を進めた。その第3は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析するツールの方法論の開発である。論理推論体系を(通常、定理自動証明の分野で行われているように)ボトムアップ的に用いると、我々の完全性定理を適用することにより、論理的に証明できない命題に対しては、その反例がシステマティックに生成される。この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると、その反例となるプロセススケジュール(プラン)、即ち安全なブロセススケジュール(プラン)の具体例が自動的に生成・枚挙される手続きが得られるのである。この考え方に基づいて、与えられた実時間システム内での種々のプラニングの問題の論理的な分析ツールの方法論を開発した。

The logic method is used to realize the theory of informatics, and the purpose of this research is to complete the research. And the theory of information technology related to the implementation of the problem to study. Second, the characteristics of the logic of the identification system and the theory of construction. The first part is the development of methodology for automatic verification of system design, system logic, system security, system selection, system selection, etc. This is the first step in the development of methodology for PSPACE determinism in a logical proof system. The second part of this paper is the discussion of the characteristics of evolution and development. The number of time constraints is increasing, and the time constraints are changing (e.g., the conditions are changing). The actual time is changing, and the daily time is changing. The third part is the development of methodology for analyzing the logic inference system of the system of safety and security. Logical inference system (usually, theorem automatic proof of the line of division, etc.) indicates that the system is not suitable for use, the completeness theorem is applicable, etc., logical proof of the system is not suitable for proposition, etc. The logical inference system holds the basic concept of "dangerous state" and the specific example of "safe state" is automatically generated. The methodology for analyzing the logic of the problem is developed in this paper.

项目成果

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：“轻线性逻辑的相位语义”理论计算机科学。

岡田光弘: "オントロジー工学の論理的基礎IV「オントロジー応用のための方法論の考察と展望」"人工知能. 17巻5号. 604-613 (2002)

Mitsuhiro Okada：“本体工程的逻辑基础 IV“本体应用方法论的考虑和展望”，第 17 卷，第 5 期。604-613 (2002)

岡田 光弘, 長谷部 浩二: "線形論理によるセキュリティ・プロトコルの論理的検証法"電子情報通信学会「人工知能と知識処理」研究会報告集. 102. 49-54 (2002)

Mitsuhiro Okada、Koji Hasebe：“使用线性逻辑的安全协议的逻辑验证方法” IEICE“人工智能和知识处理”研究组报告 102. 49-54 (2002)

K.Hasebe, M.Okada: "A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic"Hot-topic series. 2609号. 422-445 (2003)

K.Hasebe，M.Okada：“基于线性逻辑和BAN逻辑的安全协议的逻辑验证方法”热门话题系列第2609. 422-445（2003）。

岡田光弘: "オントロジー工学の論理的基礎III「現代のフォーマルオントロジーの動向とオントロジー工学」"人工知能. 17巻4号. 434-442 (2002)

Mitsuhiro Okada：《本体工程的逻辑基础 III“现代形式本体趋势与本体工程》”人工智能，第 17 卷，第 434-442 期。