Theory of formal specification and verification of concurrency systems and real-time systems based on linear logic

基于线性逻辑的并发系统和实时系统的形式化说明与验证理论

• 批准号: 12480075
• 负责人: OKADA Mitsuhiro
• 金额: $ 4.8万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2000
• 资助国家: 日本
• 起止时间: 2000 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-12480075/
• 关键词: Linear Logic; Formal Verifieation; Formal Specification; Real-Time System; 定時間システム

We gave a logical method for formal specification and formal verification of concurrent systems, in particular real-time concurrent systems, which contains quantified time constraints in the dense-time setting.In the first half of the project we gave a concrete algorithm for verification of the basic safety and other related properties (the membership property, the appointment property, the liveness property, etc.) in the dense real-time setting. We also gave a theory of automated transformation from a specification (written in the framework of natural description language) into a linear logical specification.Then in the second half of the project we extended our theories to dynamic real-time systems where the number of agents/participants and the form of time-constraints are dynamically changed. We also compared our linear logical method with the traditional model checking and the timed automata method.

我们提供了一种合乎逻辑的方法，用于正式规格和正式验证并发系统的正式验证，特别是实时并发系统，该系统包含量化的时间限制。在该项目的上半部分中，我们提供了一个具体的算法，以验证基本安全性和其他相关属性（成员资格财产，任命财产，Livice Property，Livese Property等）的现实时间。我们还将自动化转换的理论从规范（以自然描述语言的框架编写）为线性逻辑规范进行了理论。然后，在项目的后半段，我们将理论扩展到了动态的实时系统，在该系统中，代理/参与者的数量和时间构成的形式以及动态变化。我们还将线性逻辑方法与传统模型检查和定时自动机方法进行了比较。

项目成果

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

Mitsuhiro Okada：“本体工程的逻辑基础III“现代形式本体趋势与本体工程””人工智能。17。434-442（2002）

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

Mitsuhiro Okada：“本体工程的逻辑基础IV“本体应用方法论的考虑和展望””人工智能17。604-613（2002）

F. Blanqui, J-P. Jouannaud, Mitsuhiro Okada: "Inductive Deta Type Systems"Theoretical Computer Science. 272. 41-68 (2002)

F.布朗基，J-P。

Mitsuhiro Okada: "Lecture Series: Object Modeling in Philosophy and AI Research (3): Recent Developments of Formal Ontology and Ontology Engineering (in Japanese)"Journal of the Japan Society for Artificial Intelligence. vol.17,no.4. 434-442 (2002)

Mitsuhiro Okada：《讲座系列：哲学和人工智能研究中的对象建模（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逻辑的安全协议逻辑验证方法》热点话题系列。