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

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

• 批准号: 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は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析するツールの方法論の開発である。論理推論体系を(通常、定理自動証明の分野で行われているように)ボトムアップ的に用いると、我々の完全性定理を適用することにより、論理的に証明できない命題に対しては、その反例がシステマティックに生成される。この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると、その反例となるプロセススケジュール(プラン)、即ち安全なブロセススケジュール(プラン)の具体例が自動的に生成・枚挙される手続きが得られるのである。この考え方に基づいて、与えられた実時間システム内での種々のプラニングの問題の論理的な分析ツールの方法論を開発した。

该研究主题的目的是从基于信息的角度使用逻辑方法来完成实时系统验证的理论。他还研究了与该理论实施有关的信息学问题。我们已经构建了具有以下特征的逻辑验证系统的理论：首先是与整个实时系统的设计相关的系统和逻辑形式规范方法的发展，以及对实时系统的安全性和反应性，各种调度问题的安全性和反应性的自动验证方法。第二个是对进化论特有的验证和分析有效性的检查，开发了允许动态变化的实时系统。尽管增加了代理的数量，但动态时间限制可能会改变（例如，在某些条件下可能会发出截止日期的通知），在实时系统中可以每天都会发生，但我们一直在开发一种可以应用于这种动态和现实的实时系统的逻辑验证工具的方法。第三，我们正在开发一种使用我们的逻辑推理系统来分析特定计划（过程时间表）的工具的方法，在已知具有某些危险情况的实时系统中是否安全。当以自下而上的格式使用逻辑推理系统（通常在自动定理的字段中进行），通过应用我们的完整定理定理，可以系统地生成反示例，以用于无法在逻辑上证明的命题。当将此逻辑推理系统的基本机制应用于显示危险情况的命题时，该程序反例程序时间表（计划），即安全过程时间表（计划）的特定示例，自动生成并引用。基于这个想法，我们开发了一种用于在给定实时系统中各种计划问题的逻辑分析工具的方法。

项目成果

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）。

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，热门话题系列。

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

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