论文部分内容阅读
当前，软硬件系统的正确性验证问题已经成为工业界和学术界共同关注的一个大问题。模型检测作为一项对有限状态系统的性质进行自动验证的技术，是验证过程中主要采取的方法之一。它是形式化方法的一个重要分支，也是形式化方法中在工业界得到承认的一个重要范例。自20世纪80年代问世以来，模型检验技术已经取得了许多突破性的进展。它不仅已成功地应用于硬件系统和通信协议的验证上，还在软件验证方面取得了长足的进步。
实时系统是指运行过程和输出结果与时间密切相关的软硬件系统。许多反应式系统和分布式系统都属于实时系统。对于这类系统，在设计和应用的早期进行正确性验证更显得尤为重要，模型检测方法也具有更大的意义。随着实时系统的日益多样化和复杂化，要想准确而有效地描述和验证实时系统的正确性，就必须对基本模型和基本时态逻辑进行与时间相关的扩展。
本文主要研究离散实时系统的描述和验证，对模型和时态逻辑进行了离散时间的定量扩展，使它们能描述离散实时系统中具有的一些定量特征及其正确性，并设计了相应的模型检测算法。我们还研究了在线模型检测方法在无线射频识别技术(RFID，Radio Frequency Identification)中的应用。这些工作中主要用到了Pandya提出的带量词的离散时间时段演算(QDDC，Quantified Discrete—timeDuration Calculus)，它具有很强的对离散实时系统定量描述的能力。
本文具体工作和创新性如下：
1.本文提出了一种新的时态逻辑CTL[k—QDDC]，在CTL的基础上同时扩展了描述分支过去和离散时间定量性质的能力。目前对时态逻辑在描述状态过去行为方面的扩展研究大多采取的是线性过去的角度，而本文采取分支过去的角度进行扩展，不仅完善了在过去和定量两方面同时对基本时态逻辑进行扩展的理论，在描述和验证离散实时系统中的一些性质方面也具有很大的现实意义。该逻辑中还引入了有界模型检测的思想，充分利用了CTL和QDDC各自在描述性质方面的特点和优势，体现了CTL和QDDC之间的分工与互补，找到了一种可行的时态逻辑表达能力和验证复杂度之间的权衡方法。
2.本文提出了一种新的模型，圈带权的Kripke结构(Cycle—Weighted KripkeStructure)，简称为CWKS。它在Kripke结构中的一些转换上增加了两个整数的权函数，对Kripke结构中一些圈在系统实际运行过程中的重复执行次数进行了限制。这种带权圈的思想在描述实时系统中一些复杂的离散时间定量特征方面具有重要的意义。在CWKS的基础上，本文还提出了剪枝计算树的概念，定义了基本时态逻辑在剪枝计算树上的满足关系，并给出了在CWKS的一个子集上的CTL显式模型检测算法。
3.本文提出了一种形式化的RFID复杂事件描述语言QDDCatt。它在QDDC的命题变量上增加了属性以及与属性值有关的约束条件，以区分属于相同类型的不同的RFID简单事件。而QDDC操作符的引入使得这种语言在描述具有离散时间定量特征的RFID复杂事件上具有很强的能力。更重要的是，QDDCatt不仅具有RFID事件语义，可形式化地描述复杂事件的构成，它还具有逻辑语义，可把复杂事件的发生问题转化为逻辑公式在状态序列上的满足问题。在此基础上，我们还给出了一种基于QDDC自动机判定过程的RFID复杂事件的自动检测方法，它也可以看成一个在线模型检测的过程。