International collaborative studies on a logical specification and verification language.

逻辑规范和验证语言的国际合作研究。

• 批准号: 13558031
• 负责人: OKADA Mitsuhiro
• 金额: $ 4.29万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-13558031/
• 关键词: Real Time Systems; Formal Specification; Formal Verification; Linear Logic; Proof Search; 証明論

We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.

我们开发和设计了一个正式的规范和验证工具的动态实时系统的合作与法国的合作伙伴组（Jean-Pierre Jouannaud的组），基于线性逻辑。动态实时系统是指参与的Agent数量和时间约束可以动态变化的多Agent系统。我们给出了一个自动化的转换过程，将用户级的自然规范转换为线性逻辑规范。我们还给出了一个消除过程，以消除从线性逻辑规范的密集时间概念。然后，根据线性逻辑片段的证明搜索机制执行各种验证。密集时间消除过程是由构造性逻辑中已知的程序提取方法给出的。我们还开发了一个逻辑框架的安全协议的正确性证明，应用相同的概念。我们还研究了一些相关的逻辑研究，我们的线性逻辑，这是我们的验证工具的逻辑框架。

项目成果

eds.M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security -- Theories and Systems, Lecture Notes in Computer Science, Hot Topics No.2609"Springer-Verlag. 470 (2003)

eds.M.Okada、B.Pierce、A.Scedrov、H.Tokuda、A.Yonezawa：“软件安全——理论与系统，计算机科学讲义，热门话题 No.2609”Springer-Verlag。

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

F.布朗基，J-P。

M.Okada, M.Kanouchi, A.Scedrov: "Phase Semantics for Light Linear Logic and Semantic Cut-Elimination Proof"Theoretical Computer Science. (近刊). (2002)

M.Okada、M.Kanouchi、A.Scedrov：“轻线性逻辑的相位语义和语义剪切消除证明”理论计算机科学（即将出版）。

M.Okada, F.Blarqui, J-P Jouannaul: "Inductive Data Type Systems"Theoretical Computer Science. 272. 41-68 (2002)

M.Okada、F.Blarqui、J-P Jouannaul：“归纳数据类型系统”理论计算机科学。

岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17・2. 224-231 (2002)

冈田光宏：“本体论的哲学和逻辑背景”人工智能学会杂志17・2（2002）。