带有时钟变量的线性时序逻辑与实时系统验证  

A Linear Temporal Logic with Clocks for Verification of Real-Time Systems

作　　者：李广元[1] 唐稚松[1] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《软件学报》2002年第1期33-41,共9页Journal of Software

基　　金：国家自然科学基金资助项目(60073020);国家九五重点科技攻关项目(98-780-01-07-01);国家863高科技发展计划资助项目(863-306-ZT02-04-1)~~

摘　　要：为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.In order to specify real-time systems, many temporal logics such as Timed Computation Tree Logic, Metric Interval Temporal Logic and Real-Time Temporal Logic have been proposed. Although these logics are good at specifying properties of real-time systems, they are not suitable for describing the implementations of such systems. Thus, the specifications and the implementations are usually described by different languages for real-time systems. In this paper, a new linear temporal logic with clocks, called LTLC, is introduced. It is an extension of Manna and Pnueli抯 linear temporal logic. It can express both the properties and the implementations of real-time systems. With LTLC, systems can be described at many levels of abstraction, from high-level requirement specifications to low-level implementation models, and the conformance between different descriptions can be expressed by logical implication. This aspect of LTLC will be beneficial to the verification and the stepwise refinements of real-time systems.

关 键 词：实时系统 线性时序逻辑 系统描述语言 性质验证 时钟变量 计算机控制系统 

分 类 号：TP273.5[自动化与计算机技术—检测技术与自动化装置]