実時間システムの形式仕様・検証のための新しい論理的方法論

实时系统的形式化规范和验证的新逻辑方法

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

第2年次は,申請者がこれまでに確立した,線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する,証明のPSPACE決定可能性と(表示的意味論に対する)完全性という二つの定理を用いて,論理的手法による実時間システムの開発ツールを実装した.われわれのツールは次の特徴を持つ.1.その第1は,ひとつの実時間システム全体の設計に伴う,システマティックな論理的形式仕様および,われわれの(PSPACE)決定手続きを用いた安全性・信頼性の自動検証が可能である.これは,これまでに得られた上記二つの論理的基本定理を用いることにより直接遂行できた.2.その第2は,すでに与えられている実時間システムに新たな部分を加えたり,ある部分を変更したりするときに必要となる形式検証の問題や,二つの独立に作られた(安全性がそれぞれに対して保証されている)実時間システムを統合・総合しようとするときに必要となる形式検証の問題である.われわれの論理的な仕様・検証の枠組みは,もともと高度のモジュラー性を有しているので,このような問題に対しても本質的に上記1の方法論を応用することができた.3.その第3は,一部に危険な状態が生じ得ることが分かっている実時間システムのなかで,ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析する手法の開発である.論理推論体系を(通常,定理自動証明の分野で行われているように)ボトムアップ的に用いると,論理的に証明できない命題に対しては,その反例がシステマティックに生成される.この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると,その反例となるプロセススケジュール(プラン),即ち安全なプロセススケジュール(プラン)の具体例が自動的に生成・枚挙される.この手法を用いて,与えられた実時間システム内での種々のスケジューリングの問題の論理的な方法論が適用できることとなった.このようなことは,これまでの伝統的なモデルチェッキングの手法では不可能なことであった.

第二年使用逻辑方法使用申请人建立的两个定理实施了实时系统开发工具：PSPACE的确定性和基于线性逻辑的正式系统（有限的实时并行系统规格和验证）的正式系统的完整性（用于显示语义）。我们的工具具有以下特征：1。首先是使用系统的逻辑形式规格以及与整个实时系统设计相关的（PSPACE）决策程序的安全性。 - 可以自动验证可靠性。这可以直接使用迄今为止获得的两个逻辑基本定理来实现。 2。第二个是正式的验证问题，在将新零件添加到给定的实时系统或修改某些零件时是必要的，以及在集成和组合两个独立创建的实时系统（每个人都可以保证每个）时所必需的正式验证问题。我们的逻辑规格和验证框架最初是复杂的。由于其模块化，上面提到的方法可以实质上应用于此类问题。3.3。第三是使用我们的逻辑推理系统来分析特定计划（过程时间表）在已知具有某些危险情况的实时系统中是否安全的方法的开发。在实时系统中，逻辑上的推理系统以自动的构图为单位，而在构图中，这是在构图中所做的。是系统生成的。当将此逻辑推理系统的基本机制应用于显示危险情况的命题时，会自动生成和枚举的反例程序时间表（计划），即安全的过程时间表（计划）。使用此技术，可以应用给定实时系统中各种调度问题的逻辑方法。到目前为止，传统模型检查方法一直是不可能的。

项目成果

F.Banqui,J-P.Jouannaud and M.Okada: "Calculus of Inductive Construction"Proc. of Rewriting Technique and Application(RTA99),Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)

F.Banqui、J-P.Jouannad 和 M.Okada：“归纳构造微积分”Proc。

M.Nagayama,M.Okada: "A Linear Time Characterization Theorem for Non-Commutative Linear Logic"Journal of Symbolic Logic. (近刊).

M.Nagayama、M.Okada：“非交换线性逻辑的线性时间表征定理”符号逻辑杂志（即将出版）。

M.Okada and P.J.Scott: "A Note on Rewriting Theory for Uniqueness of Iteration"Journal of Theory and Applications of Categories. 6. 47-64 (1999)

M.Okada 和 P.J.Scott：“关于迭代唯一性重写理论的注释”范畴理论与应用杂志。

M.Kanovich,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).

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

M.Nagayama,M.Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. (近刊).

M.Nagayama、M.Okada：“非交换线性逻辑乘法片段的图论表征定理”理论计算机科学（即将出版）。