QRDChecker:一个QRDC模型检验工具  

QRDChecker:A Model Checking Tool for QRDC

作　　者：裴玉[1] 徐启文[2] 李宣东[1] 郑国梁[1] 

机构地区：[1]南京大学计算机科学与技术系,江苏南京210093 [2]澳门大学科技学院

出　　处：《软件学报》2005年第3期355-364,共10页Journal of Software

基　　金：国家自然科学基金;国家重点基础研究发展规划(973)~~

摘　　要：反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如 LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporallogic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将 其 实 现 为 一 个 针 对 时 段 时 序 逻 辑 QRDC(quantified RDC (restricted duration calculus))的 检验工具QRDChecker.QRDChecker 可以检验 QRDC 公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将 QRDC 公式转换成模型检验系统 Spin 能够接受的自动机的形式,从而可以检查反应式系统是否满足用 QRDC 公式表达的性质.A reactive system does not terminate and its behaviors are typically defined as a set of infinite sequences of states. In formal verification, a requirement is usually expressed in a logic, and when the models of the logic are also defined as infinite sequences, such as the case for LTL (linear temporal logic), the satisfaction relation is simply defined by the set containment. However, this satisfaction relation does not work for interval temporal logics, where the models are finite sequences. In fact, for different interval based properties, different satisfaction relations are sensible. Two classes of finitary properties are identified, and then two satisfaction relations are defined for them, which are unified by a general relation. A model checking algorithm is proposed and implemented in a verification tool for QRDC (quantified RDC (restricted duration calculus)), which is an interval temporal logic. The tool QRDChecker can check the validity of QRDC formulae under both continuous and discrete interpretations. Moreover, for discrete QRDC, it can also translate the formulae into an automaton in the form accepted by the Spin model checking system, which can be subsequently used to verify a reactive system against properties expressed in the logic.

关 键 词：模型检验 有限性性质 反应式系统 时段时序逻辑 

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