基于时间区间时序逻辑的实时系统统一模型检测  

Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic

作　　者：朱维军[1,2] 乔芃喆[3] 周清雷[1] 张海宾[2] 

机构地区：[1]郑州大学信息工程学院,郑州450001 [2]西安电子科技大学计算机学院,西安710071 [3]河南牧业经济学院信息工程系,郑州450011

出　　处：《电子科技大学学报》2014年第5期712-716,共5页Journal of University of Electronic Science and Technology of China

基　　金：国家自然科学基金(U1204608;U1304606;61373043);中国博士后科学基金(2012M511588)

摘　　要：在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此,该文使用一个离散时间区间时序逻辑公式建立实时系统模型,使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质,在此基础上,离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题。该文证明了新方法的有效性以及正确性,为区间实时逻辑这一类的模型检测问题提供了方法。There is no method for model checking real-time systems within the same real-time interval logic. To this end, we restrict a real-time logic, called Timed Interval Temporal Logic （TITL）, on discrete time domain. And then, we use a TITL formula to construct an interval model and another TITL formula to describe an interval property. On the basis of this, we formalize a novel approach for model checking within the same logical framework based on TITL. The validity and correctness of the method are proved at last.

关 键 词：统一模型检测 实时系统 可满足性判定 时间区间时序逻辑 

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