模型检查是一个有吸引力的技术，这是因为验证过程必须是自动的。然而，基于详尽的状态探索方法要求被分析的系统状态空间是有限的。有界模型检验程序把系统模型编码成逻辑公式，并利用满意度求解器搜索给定属性的反例。工具，如BarceLogic^[38]、CVC精简版^[39]、MathSAT^[40]、Yices^[41]或Z3^[42]集成了满意度求解，使用了组合理论的决策程序，这些理论包括实数和整数的线性算术等理论，因此提供了满意度取模理论。这些SMT求解器可以用于处理有界模型检测中的无限系统。有界模型检查是一种主要用于反驳而不是验证的技术。但是，它可以通过k归纳推广用来证明安全属性。

15.4.2.1 状态空间探索

由于模型检测是一种自动技术，它可以提供属性验证失败的反例，所以它可以很好地用于容错算法设计中。在算法设计过程中，算法的变动或它的参数是根据一些执行方案或不同的故障情况进行探索。挑战是对大量的这种情况下获得模型检测实验的快速反馈，进而实现设计空间的一个交互式的探索。为此，要注意把模型的状态空间保持在一个可行的尺寸上。由于设计变成综合型的，所以注意力从探索转向验证，且模型检验面临的挑战成为在合理的时间内针对一个逼真的精确模型，覆盖一套真实的、详尽的方案之一。

Steiner等^[9]在TTA一个新的启动算法分析中，描述了一种控制状态空间大小的方法，因而一个单一的模型既可以用于分析探索算法的各种替代方案，又可以用于验证最终设计的鲁棒性。故障大大增加了状态空间的规模，在模型检查中，必须对此进行探索。故障确实造成了不同的行为，但也产生不同于不相关方式的状态，在某种意义上，它们被模型程序区别，但是不会对系统的行为有不同的影响。例如，一旦正确的组件从进一步考虑排除了这个节点，那么故障节点的具体状态可能不相关。在建模容错算法中，一个有价值的技巧是：一旦有故障的组件可能不影响系统的行为，那么就把它们的状态设置为固定值。在启动算法的分析中，这种机制虽然对小型或中型模型的影响很小，但是对减少大模型的状态空间是非常有用的。

为了控制出现故障的节点可以影响系统的各种方法，模型被一个特殊的变量参数化，这个变量挑选了故障节点可能会出现的故障模式。故障节点被模拟为在每个时槽内可以发送任意信息的节点，且这样一个故障节点的可能输出被划分为六种不同故障度。例如，1级程度的故障只允许故障节点有轻微故障，而最高的6级程度的故障允许节点发送用正确或不正确的语义、噪声、两个通道上的每一个都是空信息构成的冷启动信息和正常信息的任意组合。使用故障程度较小和考虑的节点数目较少，可以允许在所需的运行时间与模型检查者进行的彻底的探索之间进行综合。

然而，对于验证来说，人们感兴趣对故障进行“面面俱到”的模拟。详尽的故障仿真意味着所有假设的故障模式要进行建模，且检查所有可能出现的情况。对于启动，这意味着对于合理规模模型组，用故障程度设置到6的模型来检测算法。对于最多达5个节点的模型，Steiner等成功验证了TTA启动的正确性，即在一个有界时间内所有正确的节点会变得活跃，并对调度表中当前位置有一致的看法^[9]。(www.daowen.com)

15.4.2.2 无限状态有界模型检验

对于检查状态过渡系统是否包含一种运行，在k步到达的一种状态违反了一个给定属性P，有界模型检验是一个基本技术^[43]。这个问题可以转化为是否满足公式的问题，其中I是定义系统初始状态的属性，而T是一个转换关系。对于有限的系统，I和T被编码为布尔公式，且满意度求解器用来检查公式。无限状态有界模型检查程序依赖于决策程序，它通过判定理论的组合解决了无量纲的一阶公式。随着这些SMT求解器变得更加高效，有界模型检验作为分析系统的方法已经获得了越来越多的关注。

如果要检查的属性是□P形式的一种安全属性，这意味着P应该在系统所有可达的状态下是真的，且满足公式F的序列状态存在，那么可以得出结论，□P不是真的。然而，反过来则站不住脚，也就是说，如果F是无法满足的，不能得出这样的结论：□P为真，因为有可能一点也不存在k长度的执行痕迹，也有可能是属性对X_k是正确的，但是在一些早期的状态中背离了。对于这些情况，可以考虑通过反复增加进度k，检查每一步中P是否在任何一种状态s₀，…，s_k中被背离；然而，没有一种方法可以用来证明□P，这是因为未能找到一些长度的反例，因而并不排除有一些较长的进度。需要注意的是有界模型检验并不限于此；这个例子是为了便于说明。

实际上为了证明安全属性P，有界模型检查被扩展到k归纳。对于一个固定的进度k，需要显示在基本情况下所有从最初满足状态P开始的k长度内的所有序列状态。归纳步骤包括证明k＋1长度状态的任何序列，就是如果前k个状态满足P，那么最后一个状态也满足。在大多数情况下，不变量P需要得到强化，以使其可归纳。这样做的一个简单的方法是增加进度参数k。然而，解决相应的计算公式的难度随k指数增长，且问题最终将变得行不通。可以选择的是用附加属性Q来加强不变量，并证明在基本情况和额外假设的归纳步骤下的所有状态的序列状态都满足Q。作为充分性，Q本身必须是一个安全属性，从而在P的证明中扮演引理的角色。

Dutertre和Sorea早已使用SAL系统^[44]把k归纳法的无限状态有界模型检查应用到TTA启动算法中^[7]。他们的研究表明，复杂的努力在解决复杂证明上是必要的。例如，即使只有两个节点的算法的简化模型，那也是可靠的，它允许使用只有非常有限功能的守护者，但是k值超过20后，安全属性的证明就不再成立。运用三个简单的引理，两个节点的证明是成功的，但是当节点的数目增加至3，计算上已经是不可行的了。为了完成更多节点的证明，使用算法抽象来加强属性。为了取得适当的抽象，它们应用分离不变量技术，这也被用在TTA组成员算法的演绎证明中。通过检查启动算法是如何工作的，定义了许多的抽象配置和相应的抽象转换。为了证明抽象的正确性，建立了监控模块，用来检查抽象模型中针对每一个转换具体算法可以采取的转换。对于有一个可靠守护者和高达10节点的系统中至少一个故障节点的容错版本的启动来说，抽象的方法被证明是可行的，能够证明所需的安全属性。