基于线性时序逻辑的实时系统模型检查  

A Model Checking of Real-Time Systems in Linear Temporal Logic with Clocks

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

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

出　　处：《软件学报》2002年第2期193-202,共10页Journal of Software

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

摘　　要：模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.Model checking is an algorithmic technique for checking if a concurrent system satisfies a given property expressed in an appropriate temporal logic. LTLC(linear temporal logic with clocks) is a continuous-time temporal logic proposed for the specification of real-time systems. It is a real-time extension of the temporal logic LTL. In this paper, the model checking problem for LTLC is discrssed and a reduction from LTLC model checking to LTL model checking is presented. This reduction will enable us to use the existing LTL model checking tools for LTLC model checking. Owing to the fact that LTLC can express both the properties and the implementations of real-time systems, the LTLC model checking procedures can be used for both the property verification and the refinement verification for real-time systems with finite locations.

关 键 词：实时系统 时间自动机 线性时序逻辑 模型检查 性质验证 算法 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]