基于Petri网的计算树逻辑模型检测 pdf下载

第1章 绪论
　　有限状态并发系统涉及众多应用领域，而正确性验证是开发设计这些系统的一个重要环节，以保障这些系统后续安全可靠地运行。模型检测是针对有限状态并发系统正确性验证的重要技术之一，而 Petri 网和计算树逻辑在模型检测上均得到了广泛的应用。本章就相关研究背景和研究现状及本书的研究内容做简单综述。
　　1.1 研究背景
　　如今，计算机软硬件系统已广泛地应用于现实中的各种领域，如电子商务、医疗器械、电话交换网、航空航天控制系统等，而微小的硬件或软件缺陷很可能会引发重大的安全事故。例如，1996 年 6 月 4 日，由欧洲 12 国联合研制的 Ariane 5运载火箭在发射不到 40 s 后解体爆炸，事故调查委员会给出事故发生的原因是火箭姿态计算机出现软件错误，即在发射过程中，当 64 位浮点数转换为 16 位有符号整数时，发生了一个例外，然而例外处理代码并没有覆盖这种情况，导致火 箭姿态计算机死机，进而造成了灾难。因此，在计算机软硬件系统投入运行之前对其正确性验证是必要的和迫切的。
　　计算机软硬件系统的基本验证方法包括：模拟、测试、定理证明和模型检测。模拟和测试需要在系统实际运行前完成一些试验，不同的是模拟是在系统的一个抽象模型中完成的，而测试是在实际产品上完成的。这两种方法难以检测到所有可能的交互故障和潜在缺陷。定理证明是指应用公理和证明规则来证明系统的正确性，可以用于无限状态系统的推理。计算机科学家广泛认可定理证明的重要性，它对软件开发领域产生了深远的影响。然而，定理证明是一个耗时的过程，而且这种方法的使用者只局限于具有丰富逻辑推理经验的专家。此外，目前大部分定理证明系统的证明过程难以实现完全自动化。
　　模型检测 [1-5] 是一种有限状态并发系统的自动化验证技术。模型检测采用形式化的模型来对系统的所有可能行为进行抽象建模，使用形式化的逻辑公式来规约系统待验证的性质，以公式在模型上成立与否来判定系统是否满足其性质。整个检测过程是完全自动化的，同时具有很高的验证效率，通常只需要花费几秒钟的时间即可产生一个验证结果。虽然将范围局限在有限状态系统是模型检测的一个缺点，但是在一般情况下，可以通过模型检测与抽象、归纳相结合的方法把无界的数据结构约束到有限状态系统上，以验证无限状态系统。
　　随着社会和经济的进一步发展，效率成为核心竞争力，而并发是提高效率的一种重要手段。从云计算 [6， 7] 到物联网 [8， 9]，从高性能计算 [10， 11] 到量子计算 [12， 13]，从工业流水线 [14， 15] 到智能制造 [16， 17]，并发成为提高并行计算与处理能力的核心要素。然而，系统设计开发过程中人工因素的增多及活动之间异步并发程度的提高，更有可能导致系统功能不能完全符合设计需求，出现死锁、活锁、数据不一致、任务在期望的时间内没有得到调度或者按时被调度执行了但（由于抢占）没有在期望的时间内完成等诸多问题。例如，对一个资源分配系统，多个并发执行的任务共享一组有限资源，当一些任务均占有一些资源而又等待对方所占用的资源时，就形成了循环等待，造成死锁。因此，有限状态并发系统需要模型检测技术来保证它们的行为正确性。
　　随着计算机网络和信息技术的发展，多智能体系统 [18-20] 引起人们的广泛关注。多智能体系统是由多个交互智能体组成的计算系统，其中每个智能体既可以*立自主地完成各自的任务，又可以彼此协作地完成一个共同的任务，因此多智能体系统能够解决现实中广泛存在的复杂大规模问题。目前多智能体系统已成功地应用于智能电网、智慧交通、无人机、自动驾驶、军事集群系统等各种领域。当然，多智能体是一个很大的研究领域，而本书关注的是安全多方计算协议，它通常被看作为了确保一组智能体某种（或一组）隐私/安全属性而精心设计的满足某种规则的交互过程。安全多方计算协议的正确性不仅取决于该协议的行为正确性，还取决于每一方的隐私安全是否能够得到保障，即每一方的隐秘信息不会被另一方所获知。例如，对一个采用安全多方计算协议的电子拍卖系统，一旦投标者的标价可被某些人所获知，则很可能会导致拍卖过程彻底失去了公平性。因此，安全多方计算协议需要模型检测技术来保证它们的行为正确性和隐私安全性。
　　随着计算机硬件的飞速发展，人们对系统的设计需求也越来越高。在一些实际应用中，人们不仅要求一个系统的计算结果准确无误，而且更关注该系统产生这个结果所花费的时间长短，这就是实时系统 [21-23]。实时系统是指系统能及时地响应外部事件的请求，在规定的时间内完成对该事件的处理，并控制所有实时任务协调一致地运行。因此，实时系统的正确性不仅依赖于系统的行为正确性，而 且还依赖于行为出现的早晚。如果系统的时间约束条件得不到满足，那么系统仍然会出错。实时系统进一步分为强实时系统和弱实时系统，强实时系统是指严格遵循时间约束，超出时间限制会造成严重的功能失效的实时系统，并且这种系统失效常常会伴随着严重的财产损失甚至生命安全，目前强实时系统已应用于军事、核工业、航空航天等一些关键领域。弱实时系统在人们生活中比较常见，如信息采集与检索系统、视频点播系统等，虽然存在时间需求，但是偶尔违反这种需求对系统的运行不会造成严重影响，然而频繁违反这种需求依然会导致时间的偏移越来越大，整个系统的正确性也会随之下降。因此无论是强实时系统还是弱实时系统，都需要模型检测技术来保证它们的行为正确性和时间正确性。
　　1.2 研究现状
　　对所要验证的系统进行形式化建模是模型检测的前提。目前已有许多科学家在这方面做出了开创性的工作，创建了多种形式化模型，如 Petri 网 [24-32]、反应式模块 [33]、解释系统编程语言（interpreted systems programming language，ISPL）[34， 35]、进程代数 [36]、通信序列进程 [37]、π-演算 [38] 等，这为后续的研究和应用打下了坚实基础。Petri 网由于可以很好地刻画顺序、选择、并发和同步等关系，所以在系统的建模与验证方面取得了丰硕的成果 [39-45]。目前，Petri 网已成为模型检测领域最常用的建模语言之一 [46-50]，例如，每年的国际模型检测竞赛都选择 Petri 网作为其测试用例的建模语言。
　　对系统待验证的性质进行形式化规约同样是模型检测的前提。目前已有多种逻辑语言用于规约系统待验证的性质，但它们通常又关注不同的方面，如线性时序逻辑（linear time logic，LTL）[51， 52] 和计算树逻辑（computation tree logic，CTL）[53-57] 侧重规约时序性质，交替时序逻辑（alternating-time temporal logic，ATL）[58， 59] 和策略逻辑（strategy logic，SL）[60， 61] 侧重规约策略性质，认知逻辑（epistemic logic，EL）[62， 63] 侧重规约认知性质等。其中 CTL 广受欢迎，因而得到了长足的发展，目前已具有各种各样的扩展形式，如 CTL. [64-67]、知识计算树逻辑（computation tree logic of knowledge，CTLK）[68-72]、时间计算树逻辑（timed computation tree logic，TCTL）[73-76]、知识时间计算树逻辑（timed computation tree logic of knowledge，TCTLK）[77]、概率计算树逻辑（probabilistic computation tree logic，PCTL）[78-82]、概率知识计算树逻辑（probabilistic computation tree logic of knowledge，PCTLK）[83]、承诺计算树逻辑（computation tree logic for commitments， CTLC）[84]、承诺知识计算树逻辑（computation tree logic of knowledge for commitments，CTLKC）[85， 86] 等。正是由于 CTL 的强大功能，使其成为模型检测领域最常用的逻辑语言之一，例如，每年的国际模型检测竞赛都将 CTL 作为其测试用例待验证性质的形式化规约。
　　1.2.1 有限状态并发系统控制流的模型检测
　　对有限状态并发系统控制流的建模 [87-98] 和分析是保障有限状态并发系统正确性的必要环节，本书研究有限状态并发系统控制流的模型检测，验证有限状态并发系统控制流的行为正确性。若无特别说明，下文中的有限状态并发系统实际上是指有限状态并发系统控制流。
　　有限状态并发系统模型检测通常以原型 Petri 网为有限状态并发系统的形式化模型，以 CTL 为有限状态并发系统性质的形式化规约，以 CTL 在原型 Petri网上成立与否来验证有限状态并发系统的行为正确性。目前已经开发出相应的模型检测器，如 Tapaal [99， 100]、ITS-Tools [101]、LoLA [102， 103] 等。然而，在此过程中需要生成原型 Petri 网的完整可达图以验证 CTL 公式，这就导致了状态空间爆炸问题 [104-106]，即可达图的标识数随着原型 Petri 规模的扩大而呈指数级增长，而目前计算机的中央处理器（central processing unit，CPU）和内存显然无法计算和存储如此庞大的数据，从而导致模型检测技术在面对较大规模的有限状态并发系统时无能为力。因此，需要寻找一种符号化的方法来隐式表示可达图以提高模型检测的可用性和实用性，简化有序二叉决策图（reduced ordered binary decision diagrams，ROBDD）[107-112] 即是其中最典型的代表之一。ROBDD 作为一种新型数据结构，不仅可以实现用较小的数据结构表示较大的集合，而且可以实现集合之间的各种高效运算如集合的交并补等操作。因此，ROBDD 不仅可以符号存储可达图的标识集和标识迁移对集，而且可以实现在符号化的可达图上验证 CTL 公式，这种通过 ROBDD 符号表示整个模型检测过程的技术被称为符号模型检测 [5， 104]。注意，除了 Petri 网这种形式化模型，还可以采用其他的形式化模型来描述有限状态并发系统，如模型检测器 SPIN [113， 114] 所定义的进程元语言，模型检测器 NUSMV （new symbolic model checker）[115， 116] 所定义的一种描述有限状态并发系统的输入语言。这些非 Petri 网的形式化模型在有限状态并发系统具有很高的并发程度时更容易在建模的过程中出现状态空间爆炸问题，而Petri 网可以直观地刻画并发行为，因此可以避免这样的问题。
　　ROBDD 所具有的这一切优势是假设它不会出现节点爆炸问题。ROBDD 的节点爆炸问题是指 ROBDD 的节点数随着其变量数的增加而呈指数级增长，在*糟糕的情况下，一个由 n 个变量组成的 ROBDD 可以包含 2n 个节点。避免 ROBDD 节点爆炸问题的一个关键因素就是为其寻找一个合适的变量序，然而找到一个性能最优的变量序在复杂性理论上是 NP-困难的 [117]，甚至判定一个给定的变量序是否是性能*优的在复杂性理论上也是 NP-完全的 [118]，因此人们通常寻找一个性能良好的变量序而非性能最优的变量序。目前寻找 ROBDD 变量序的方法主要分为两种类型，即动态变量排序法 [119] 和静态变量排序法 [120， 121]。动态变量排序法通过多次调整一个已经建好的 ROBDD 变量序来进一步减少 ROBDD 的节点数，该方法的时间复杂度较高且*终生成的 ROBDD 变量序效果并不理想。