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

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

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

In the 2nd year, the applicant established the basic theory of linear logic (finite state), the theory of time parallelism, the formal system of proof, the completeness of PSPACE decision possibility (meaning theory of representation), the application of two theorems, and the implementation of logical methods for the development of time parallelism. 1. The first part of the design, the actual time, the whole design, the logical form, the automatic detection of the reliability, the security, the reliability, the possibility of the manual detection. The basic theorem of logic is used directly. 2. The second part of logic is used directly. 3. The second part of logic is used directly. 4. The third part is used directly. 2. Independent work (safety and security), integration, integration, and necessary formal verification issues. The logic of the problem is that the problem is the result of the problem. The problem is the result of the problem. The concrete analysis method is used to develop the logical inference system for safety. Logical inference system (usually, theorem automatic proof of the line The logic inference system holds the basic concept of danger state, and the counter example of danger state is automatically generated. This method is applicable to the methodology of logic of problems in time systems. This is the first time I've ever seen a woman who's been in a relationship with someone else.

项目成果

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. Okada: "Theories of Types and Proofs, second edition, Memoir of mathematical Society of Japan Vol.2"Mathematical Society of Japan. (1999)

M. Okada：“类型和证明的理论，第二版，日本数学会回忆录第2卷”日本数学会。

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