Research on Specification and Verification of real-time software

实时软件规范与验证研究

• 批准号: 07680341
• 负责人: YONEZAKI Naoki
• 金额: $ 1.47万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07680341/
• 关键词: Real-time Software; Secification; Verification; Temporal Logic; Real-time Logic; Linear Logic; Relevant Logic

It became crucial issue to build correct software with real time feature for safe critical systems e.g.embedded software in control systems. In order to make these software safer and securer, we need a new software construction method based on verification technique. In this research project we had the following results.1) Proof systems of temporal logic for various time domainsFirst we developed connection calculus for temporal logic with discrete time domain. To prove the validity of a formula in discrete frames, we have to check the unsatisfiability for infinite frames. This means that we need substituion for infinite length of modal operators in connection calculus. In our approach we allows self substitution for modal operators so that we can solve the problem.Then next we studied axiomatic systems for a temporal logic with real number timed domain. We showed that it is neither possible to construct complete axiomatic system nor to give decision procedure for the validity of a formula. We restricted it to rational domain where the number of the charge of state is bounded, as a result we had decidable logic.2) Various aspects of software verification2-1) Differential verification method for temporal specificationWe developed new tableau method for differential verification, where the verification result for the previous specification is reused with the difference between a new specification and the previous one.2-2) Level of realizabilities of a specification and its decision procedureWe defined several concepts approaching realizability. The classification of specifications based on these concepts gives us useful information for making a specification realizable. We gave the decision procedure for the membership of the classes and also we had an idea to identify a set of the parts of the specification which is the cause of un-realizability.

对于安全的关键系统，如控制系统中的嵌入式软件，如何构建正确的具有真实的时间特性的软件成为关键问题。为了使这些软件更加安全可靠，需要一种新的基于验证技术的软件构造方法。在本研究项目中，我们取得了以下成果：1）时态逻辑在不同时间域的证明系统首先，我们发展了时态逻辑在离散时间域的连接演算。为了证明一个公式在离散框架中的有效性，我们必须检查无限框架的不可满足性。这意味着我们需要替换连接演算中无限长的模态算子。在我们的方法中，我们允许模态算子的自替换，这样我们就可以解决这个问题。接下来，我们研究了具有真实的数域的时态逻辑的公理系统。证明了既不可能构造完备的公理系统，也不可能给出公式有效性的判定过程。2）软件验证的各个方面2 - 1）时间规格说明的差分验证方法我们发展了新的差分验证的tableau方法，其中，重新使用先前规范的验证结果，并保留新规范与先前规范之间的差异。2 - 2）规格说明的可实现性水平及其决策过程我们定义了几个接近可实现性的概念。基于这些概念的规范分类为我们提供了使规范可实现的有用信息。我们给出了类的成员的决策过程，并且我们有一个想法来确定规范的一组部分，这是不可实现的原因。

项目成果

Yoshiaki Minamisawa and Naoki Yonezaki: "Model based semantics for linear logic CLLe" 55th Conference Proceedings Information Processing Society of Japan. 547-548 (1997)

Yoshiaki Minamisawa 和 Naoki Yonezaki：“基于模型的线性逻辑 CLLe 语义”第 55 届日本信息处理学会会议论文集。

Shigeki Hagihara and Naoki Yonezaki: "Improving efficiency of modal theorem prover by informations from the failure of the past proof process" 12th Conference Proceedings Japan Society for Software Science and Technology. 105-108 (1995)

Shigeki Hagihara 和 Naoki Yonezaki：“通过过去证明过程失败的信息提高模态定理证明器的效率”第 12 届会议论文集日本软件科学技术学会。

須藤忠祐、米崎直樹: "実時間論理RTL^Qの公理化に関する研究" 日本ソフトウェア科学会第14回大会論文集. 381-384 (1997)

Tadasuke Sudo、Naoki Yonezaki：“实时逻辑 RTL^Q 公理化研究”日本软件学会第 14 届年会论文集 381-384 (1997)。

Yoshiaki Minamisawa,Masahiko Tomoishi,Naoki Yonezaki: "Semantics for Linear Logic and its Completeness" The 6th European-Japanese Conference on Information Modelling and Knowledge Bases. (1996)

Yoshiaki Minamisawa、Masahiko Tomoishi、Naoki Yonezaki：“线性逻辑语义及其完整性”第六届欧洲-日本信息模型和知识库会议。

米崎直樹,鈴木康人,須藤忠祐: "実時間論理RTL" 日本ソフトウェア科学会第12回大会論文集. 137-140 (1995)

Naoki Yonezaki、Yasuto Suzuki、Tadasuke Sudo：“实时逻辑 RTL”日本软件学会第 12 届年会论文集 137-140 (1995)。