论文部分内容阅读
模型检测最重要的特性之一是能够为不满足的时态属性生成反例。反例可以为工程师提供调试信息,以进一步解释属性的违反情况。然而,在模型检测的发展中,迄今为止对反例的研究依然很少。已有的最先进的符号化模型检测工具在规范描述上表达力不足,仅能验证实时时态认知逻辑的小部分子集,而且产生的反例相对简单、不完整、并且缺乏便于理解的注释。为此,本文首次提出了一种新的实时分支时态认知逻辑RTCTL~*K,它是计算树逻辑CTL~*结合了实时区间和认知的扩展,使得实时相关性质、智能体认知状态及两者共同作用下,即某时间区间内智能体的认知可达关系可以被方便地描述和验证。然后我们给出了基于测试器的符号化反例生成算法,深度改进并实现了新的模型检测工具,使其能够自动为RTCTL~*K生成足够简洁的图形化反例,更易于直观分析。本文主要研究工作包括定义RTCTL~*K的语法语义,给出反例生成算法并实现符号化模型检测工具—MCTK2,具体如下:(1)我们定义了表达能力更强的实时分支时态认知逻辑RTCTL~*K,它是CTL~*的一个扩展,同时具有离散的时间区间和认知逻辑。(2)基于公平性离散系统JDS,我们设计了RTCTL~*K的反例生成算法。生成的反例是具有分支结构的有向状态迁移图。为便于理解,在图中的状态和迁移关系上附有一些满足的子公式来加以注释,每个强连通的分量都是一个循环,对应的分量图是树状结构。而且,为避免产生庞大的树状模型图,子公式的证据将依据用户需要而交互式产生。由于图上每个节点均是可交互的,对于附加在状态上的每个未解释的子公式(前面含有路径量词或认知算子),当用户单击该状态时,从当前状态会创建出新的分支。而且对于JDS上RTCTL~*K的全称片段,我们证明了其反例生成算法的完备性。(3)开发了一个符号化模型检测工具MCTK2,并实现了RTCTL~*K的反例生成算法。通过与著名的模型检验器nuXmv和MCMAS进行一系列实验比较,分析结果表明,相比于nuXmv,MCTK2在验证RTLTL公式并产生反例的时间效率上优于nuXmv,在易用性以及验证CTL~*K、RTLTL、RTCTL~*公式并产生反例的时间消耗和内存占用方面均优于MCMAS。