建立容错系统模型包括相对系统提供的容错性能故障的故障假设的慎重考虑。故障假设包括可能发生的各种故障的假设、故障出现频率和可以容忍的故障总次数。

混合故障模型^[24，25]可以区分不同严重程度的各种类型故障。例如，可以被无故障节点持续检测到的故障是不太严重的，被称为是良性的，或明显故障。对称性故障一般不会被立即检测到，但每个无故障节点会观察到相同的行为。最严重的故障类型是不对称故障，它可能对不同的无故障节点显示出不同的行为。

TTA的主要故障假设是单故障假设，即该架构可以容忍它的组件之一的任意故障。最近，一个新的更广泛的解决多个组件的瞬态故障的故障假设已经被讨论^[26]。它依赖于一个允许系统排除故障节点短暂混乱后重构的强大的派系解决算法。

对于发生故障组件，存在更多的设计选择。例如，故障模型可以包括链接故障来形容通信通道的故障。或者，通道可以被看做是属于发送方或接收方，可以通过把故障归因到特定节点来抽象通道故障。例如，TTA组成员算法的分析只考虑故障节点（它可以是发送故障或接收故障）。Pike等^[27]抽象节点故障为只影响一个节点的发送能力，以便节点接收信息失败最终体现为该节点的发送故障。

相对于一般的故障模型，可以进行基于定理证明的演绎分析。Pike等^[27]提出各种抽象，便于建模和分析容错系统，其中包括描述故障及其对节点发送和接收各条信息正确性影响的抽象。在他们的模型中，存在两种类型的抽象信息：接收的信息携带接收节点可以提取的相关的信息数据m，然而所有检测到的不正确信息被抽象为一个单一的良性信息。故障采用函数send进行抽象建模，该函数根据以下故障状态，描述节点r从发送方s接收的抽象信息：(www.daowen.com)

accepted（m）如果status（s）＝good

在没有进一步的属性被假定为接收的特定信息时，函数sym和asym在某种意义上是不能解释的。但是，在sym的情况中，可以推导出所有节点都接收同样的尽管是未知的信息，而对于两个接收器r和r′，asym（m，s，r）表示的信息一般是不等于asym（m，s，r′）。因此，不对称故障节点的故障行为是完全不明的。

与故障建模的陈述方法不同，故障的影响必须在一个模型检查背景中被明确地建模。例如，建立非对称发送故障模型，需要允许一个节点发送不同的信息到不同的节点。用于模型检验程序的规范语言通常支持表达从一个给定的基组中不确定性选择一个元素，因此不对称发送故障节点可以为每个接收节点通过不确定性选择信息来建立模型。