面向实时系统的实时区域时态逻辑：RRTL

摘要

为了描述实时系统的性质和行为，各种不同的实时逻辑如MITL、RTTL、TPTL等相继提出，在该文中，我们对此作了一个较为细致的回顾.但是不论是基于点语义的实时逻辑还是基于区间语义的实时逻辑，均不能以很直观的方式来描述实时系统，特别是对那些有事件反复出现的反应式实时系统更难于描述.基于上述考虑，在该文中，我们提出了由区间的无限序列组成的区域的概念，定义了区域的一些一元运算和二元关系.在此基础上，我们对于基本的命题线性时态逻辑PLTL的核心进行了实时扩展，给出了一个具有连续语义的实时区域时态逻辑(Real-timeRegionTemporalLogic)，简记为RRTL，定义了RRTL的语法和语义，并且给出了一个形式化的公理系统，建立了RRTL的形式化语义模型，在我们给出的语义解释下，证明了公理系统的合理性.作为它的一次实际应用，我们用它对于实时系统中的一个典型实例：GRC（GeneralizedRailroadCrossing）进行了描述，给出了它的系统规约，在此基础上，演绎式的证明了系统的一个安全性和活性命题.最后简要介绍了我们开发的一个简单的区域求解工具来辅助我们的演绎式推理.

目录

文摘

英文文摘

独创性说明

前言

第一章 ：形式化概述

§1.1形式化的开发方法

§1.2形式化方法的分类和在实际中的应用

§1.3形式化方法的发展

第二章 ：面向实时系统的形式化方法

§2.1.时序逻辑简介

§2.2实时系统的特殊性

§2.3实时逻辑

§2.4.实时系统的其他形式化方法

§2.5.小结

第三章 ：连续语义的实时区域时态逻辑RRTL

§3.1引言

§3.2区域的基本概念

§3.3 RRTL语法

§3.4RRTL语义与模型

§3.5形式化公理系统

§3.6形式化公理系统的合理性

§3.7小结

第四章 ：利用RRTL来验证一个实际实时系统

§4.1系统描述

§4.2系统的规约

§4.3系统性质的证明

§4.4小结

第五章 ：工具开发实例

§5.1一个简单的区域求解软件：Solver

§5.2 Solver的主要功能

§5.3 Solver的设计与实现

§5.4小结

结束语

参考文献

致谢