时间触发以太网拜占庭容错方法的形式化验证

汤雪乾，李 峭，孔韵雯，何 锋

（北京航空航天大学电子信息工程学院，北京100191）

1 引言

综合化计算节点是航天器电子系统的关键部件，其可靠性直接关系到航天器能否安全运行并完成预定任务。对于载人的航天器，高安全关键等级的设计要求使用冗余配置来增强航天器内计算节点容忍多种故障模式的能力，其中最具挑战性的是对于拜占庭故障的容错。

拜占庭故障（Byzantine Fault）也被称为“任意故障”，其特点在于故障节点对其他不同的节点表现出任意不同的行为［1］。要求载人航天器的分布式电子系统容忍拜占庭故障，即是要求其多个子系统或者部件满足处理和传输信息的一致性检查要求，消除局部节点故障时任意行为对于系统的危害。

经典的容忍拜占庭故障方法为口头消息算法（Oral Messaging，OM）算法［2］，即使用全交换机制在所有的节点中达成一致性，所有的节点使用通道化总线（Channelized Bus）的形式互连。通常使用4个故障封闭区（Fault Containment Region，FCR），2个轮次的数据交换，3条独立的路径可以容忍1个节点的拜占庭故障，并使用符号分析实验室（Symbolic Analysis Laboratory，SAL）进行形式化验证［3］。肖爱斌等学者对经典的拜占庭模型进行了改进，增加了网络单元（NE），并对两轮交换发送次序进行了优化，提出了一种星载计算机拜占庭容错设计方法［4］，同时也对这种方法进行了可靠性的分析［5］。 高亚楠等学者［6］提出了一种并行通道配合计算节点交联的体系结构，采用1553B和TTP数据总线，使用数据交换和数据比对达到系统故障检测和故障容错的要求。另外，还有使用可进化硬件容错智能方法来控制计算机容错［7］。这些研究成果为总线式互连的网络节点容错提供了支持。在时间触发以太网（Time-Triggered Ethernet，TTE）的研究中，也曾借鉴类似ARINC659（SAFEbus）总线的层次化拜占庭容错设计，结合自检对达到一致性［8］，但并不针对交换式链路层，属于应用层协议扩展。

航天器电子系统随着复杂程度提升，为了降低航天器平台的体积、重量和功耗（SWaP），呈现向综合模块化航电（Integrated Modular Avionics，IMA）架构发展的趋势［9］。IMA架构采用具有多个网段的交换式综合化互连技术、商用货架（Commericial Off-the-Shelf，COTS）产品和开放性接口标准，例如：美国NASA兰利研究中心提出的SPIDER架构、NASA的演进火星运动项目、猎户座多用途载人飞船（Multi-Purpose Crew Vehicle， MPCV）［10］；其中，SAE AS6802 标准［11］定义的 TTE 网络作为MPCV飞船综合化网络互连基础设施，得以实用，实现计算节点之间数据的分发和同步［12］。

载人航天器具有极严苛的可靠性和容错能力要求，简单地堆砌COTS产品无法满足该要求，必须进行适用性改造。NASA的Loveless和TTTech公司的Fidi等学者［13］提出一套时间触发网络体系结构下的拜占庭容错实施方案，基于分布式处理器和全交换体制可以容忍一个拜占庭故障。然而，现有研究［12-13］只是对时间触发网络拜占庭容错方法进行了推理论证，没有用规范性的方法进行描述与证明。虽然对OM算法的形式化验证可供借鉴，但目前尚未发现其他公开发表的文献直接使用形式化工具对该容错方法的正确性进行验证。本文在阐明基于TTE互连的航天器拜占庭容错设计的理论与方法的基础上，采用符号分析实验室（SAL）形式化工具［14］，对相应的互连配置和网络节点建立形式化分析模型，并进行模型检查（model checking），为相应容错方法的协议正确性和容错能力提供优于推理论证的规范化验证。

2 拜占庭容错

2.1 拜占庭容错的理论基础

为了使对抗拜占庭故障的冗余配置更加有效，将系统进行硬件划分，形成一个个独立的故障封闭区域（Fault Containment Region，FCR），依靠设计实现和认证评审使故障的影响和传播不跨越FCR。这样，在随后的容错方法分析论证中，设每个节点为一个FCR，即默认“节点”和“FCR”的称谓可以互相代替，则理论上容忍f个拜占庭故障必须满足以下要求［15］：

1）必须具有不少于3f＋1个FCR；

2）节点间接收消息必须通过不少于2f＋1个独立路径；

3）节点间交换消息必须通过不少于f＋1个轮次；

4）分布式节点的时钟同步必须具有一个有界的偏差。

在拜占庭一致性的要求下，所有的非故障节点必须保证如下的特性［12］：

1）一致性：所有非故障节点一致同意一个相同的值。

2）有效性：所有非故障节点都有一个相同的初值，然后所有非故障节点都一致同意。

3）终止性：所有非故障节点最终决定一个值。

2.2 经典拜占庭容错方法

经典的拜占庭容错方法是执行OM算法以保证交互一致性，节点之间使用全通道数据链路（Cross-Channel Data Link，CCDL） 形式互连［13］。为了减少成本的开销和设计的复杂度，引入一种特殊的设备，称为“级间”（interstage）［15］。 一个级间就是一个FCR，根据OM算法转发消息，但是自身并不要求一致性。级间的目的是提供执行拜占庭一致性算法的功能，但不要求所有的参与容错的FCR都是全功能的处理器［13］，如图1所示。

图1 经典拜占庭容错方法［5］Fig．1 Classical Byzantine fault tolerance method［5］

以节点读取传感器数据的过程为例，为达到交互一致性，首先节点从本地总线接口读取传感器的数据，这个步骤并不要求一致性。第一轮（R1）节点1－3发送自己的初值到其他的计算节点和级间中；第二轮（R2）节点1－3和级间发送第一轮数据到其他的计算节点中。然后节点1－3对第二轮数据执行多数制来校正第一轮的数据。非故障计算节点现在能够共享相同的交互一致性（Interactive Consistency，IC）向量。最终节点1－3执行一个选择函数来选择最终的值（该选择函数为取中位数或者取平均值）。经典的拜占庭容错利用的是全连通的独立信道，在综合化交换式互连的场景下需要进行改进。

2.3 时间触发网络拜占庭容错方法

时间触发网络拜占庭容错方法基于交换式表决架构（如图2），采用TTE网络进行数据的分发和同步。每个机载计算节点执行特定的应用层软件，与网络控制器相连接；控制器执行TTE协议所要求的服务；主机和控制器作为一个端系统，通过两个或者三个冗余TTE网络交换机实现双向连接［12］；TTE网络交换机与数据输入设备和输出设备实现全双工连接，通过点对点物理链路组成全交换（full-exchange）星型拓扑结构［12］。

另外，依据 SAE AS6802 标准［11］：高完整性的配置的节点（端系统或交换机）含有指令／监视对（COM／MON pair），在图 2 中以标有“C／M”的灰色方框表示；标准完整性的配置的节点（端系统或交换机）仅含有指令器（COM），在图2中的白色框表示未配置监视器（MON）。以计算节点读取传感器数据的过程为例，为达到交互一致性，时间触发网络算法的执行步骤如下：

图2 时间触发网络拜占庭容错方法［13］Fig．2 Byzantine fault tolerance method of time-triggered network［13］

1）（R1）每个冗余输入设备传输数据到交换机1－3。但是这并不保证非故障设备一致，一个故障设备可能任意传输数据。

2）（R2）交换机1－3发送每个冗余输入设备的消息到所有的计算节点1－3。

3）计算节点1－3对来自每个冗余网络通道的消息执行多数制表决。违反协议的消息将被丢弃。多数制必须根据接收消息的数量确定，不是静态的2／3。非故障计算节点至此共享相同的IC向量。

4）计算节点1－3执行一个选择函数来选择一个最终的值。

3 时间触发网络容错的SAL建模

3.1 SAL工具

模型检查是用形式化方法精确地证明一个系统能够按照预定目标正确工作，是一种广泛用于软硬件形式的验证工具［16］。SRI计算机科学实验室推出了一种将定理证明和模型检验等多种符号分析技术相整合的框架SAL（Symbolic Analysis Laboratory）工具。SAL框架集成了归纳、程序分析、定理证明和模型检查等工具。SAL框架的关键部分就是一种描述转换系统（transition systems）的语言，以及对这种语言描述的模型的编译和属性查找引擎。SAL提供了规范状态机和它们的属性的表达式，同时提供了模型检查器及其状态机属性分析工具。

3.2 SAL模型描述

SAL最基本的建模单元是模块。模块可以定义状态机，并通过输入变量和输出变量实现与其他模块之间的交互；在模块的内部，则通过状态变量来实现转换关系。模块可以嵌套，一个模块可以作为其它模块的一部分［17］。

使用SAL语言，建立TTE网络容错协议操作的抽象模型，包括：输入设备模块（source模块）、交换机模块（switch模块）和计算节点模块（compnode模块）；为了设置故障场景，设置了控制器模块协调各个网络组件抽象的模块，它使用stage变量控制整个网络数据交互的进程。

控制器通过设置stage变量来控制数据交互的进程（第13行）。在初始化阶段（第7－10行），设置对输入设备和交换机为无故障。控制器模块的SAL规则如图3所示。

图3 控制器模块的SAL规则Fig．3 SAL specification of controller module

设置故障时需要根据SAL的语法改写图3中第9 －10 行，如“sf＝［［j：sources］ none］；”改写为“sf［1］ ＝arbitrary”，通过不确定赋值（图 4 第17－18行）产生一个任意故障，source模块对不同的节点，发送不同的数值。SAL并没有表示消息遗漏的专用符号，因而此处用“0”代表遗漏故障（图4第14行）。

网络中数据传输的过程是：输入设备向交换机发送传感器数据，然后交换机把接收到的数据转发到计算节点中。如图4所示，在无故障的情况下，输入设备将发送正确的数据到交换机模块中（第10－11行）。在设置了故障场景的情况下，输入设备模块可以接收来自控制器模块的故障设置信息，标识自身是否故障。图4中的第13－15行定义输入设备发生遗漏故障，图4中的第17－18行定义输入设备发生任意故障。

图4 输入设备模块的SAL规则Fig．4 SAL specification of input device module

如图5所示，交换机模块接收来自输入设备发送的数据，在无故障的情况下，将数据正确地转发到计算节点模块中（第10－11行）。在设置了故障场景的情况下，交换机模块根据控制器模块设置的故障信息，标识自身是否故障。图5中的第14－15行定义交换机发生遗漏故障，图5中的第17－18行定义交换机发生任意故障。

图5 交换机SAL模型Fig．5 SAL specification of switch module

计算节点模块接收来自交换机模块转发的数据，如图6所示，然后执行多数制的表决（第15－16行调用多数制表决函数），各个计算节点最终的处理结果将达到一致。注意：在验证不一致遗漏故障时，使用%注释15－17行代码，反注释18－21行代码。

多数表决函数的关键代码如图7所示，其中以正整数v抽象地表示计算节点接收到的数值，由于“0”已经被用来代表遗漏，v参与表决的取值不包含0，而是从1开始，这种方式也与文献［12］对于故障假设的建模表达相同。

图6 计算节点SAL模型Fig．6 SAL specification of computer node module

图7 多数制投票表决算法Fig．7 SAL specification of majority vote algorithm

4 模型检查与结果分析

模型检查形式化方法不仅要对被检查的模型建模，而且还要用形式化的语言描述待验证的特性。在SAL工具中，关键字“THEOREM”所定义是断言规则，用以描述模型的属性［17］。利用SAL引擎，即可搜索检查相应的断言是否成立。

为验证时间触发网络拜占庭容错方法的正确性和有效性，在SAL建模工具中设置3个输入设备、3个交换机和3个计算节点的模型实例，互连结构如图2所示。SAE AS6802标准支持单失效假设和双失效假设，并规定端系统的故障模式为任意故障或不一致遗漏故障，交换机的故障模式为不一致遗漏故障。本文设置6种典型故障场景来验证触发网络拜占庭容错方法的正确性，分别是单失效假设下端系统的任意故障（场景1）和不一致遗漏故障（场景2），以及双失效假设下两个端系统的不一致遗漏故障（场景3），两个交换机的不一致遗漏故障（场景4），以及一个端系统和一个交换机的不一致遗漏故障（场景5）。以上5种故障场景根据SAE AS6802标准中的失效假设来设置，同时增加场景6和场景7来进一步测试时间触发网络拜占庭容错方法的容错能力。

在模型检查之前，需要对定义的SAL规则进行基本属性（活性）的检查，以保证容错协议模型不会死锁。如图8所示，通过SAL工具对上述建立的形式化模型进行活性（liveness）检查，检查结果表明，模型满足活性的要求。

图8 活性检查定理Fig．8 Liveness checking theorem

如图9所示，通过构造有效性定理和一致性定理对上述建立的形式化模型进行模型检查。结果表明，形式化模型满足有效性、一致性和终止性。表1中的故障场景1和7表明时间触发网络拜占庭容错方法能够容忍1个拜占庭故障节点，但无法容忍2个并发的拜占庭故障节点。

图9 模型检查定理Fig．9 Model-checking theorem

能够容忍1个拜占庭故障，必然可以容忍1个“不一致遗漏”故障，表1中故障场景6的检验结果印证了这一点。更进一步，在高完整性配置下，时间触发网络节点能够将拜占庭故障模式转化为不一致遗漏故障模式，为了针对性地展示TTE网络在拜占庭容错的基础上的扩展容错能力，将输入设备和交换机设置为“不一致遗漏”（inconsistent-omit）故障，作为故障场景3－5，然后验证拜占庭容错方法的有效性，实验结果表1所示。由表1可知，时间触发网络拜占庭容错方法可以容忍1个不一致遗漏故障节点或者2个不一致遗漏故障交换机节点，无法同时容忍2个拜占庭故障。由拜占庭容错理论可知，在目前的架构中，仅仅增加源端或者交换机的数量而不增加独立路径的个数无法提高架构的容错能力。

表1 算法特性分析Table 1 Characteristics analysis of the algorithm

值得说明的是拜占庭故障是最严苛的，危害程度也最高。TTE网络通过高完整性配置能够将拜占庭故障模式降级为不一致遗漏故障模式，减小了拜占庭故障的危害。TTE网络在目前时间触发架构下能够容忍一个拜占庭故障，同时依靠C／M对配置还可以容忍2个不一致遗漏故障交换机节点。理论上容忍f个严格不一致遗漏故障必须具有不少于f＋1个FCR，节点间接收消息的路径必须不少于f＋1个［12］。因此表1结果与形式化检查结果完全符合，也与理论结果相吻合。

5 结论

通过对时间触发网络拜占庭容错方法的形式化分析和验证，可以确信地掌握相应容错操作的有效性和能力，主要体现于：

1）通过SAL的模型检查，从理论上证明了时间触发网络拜占庭容错方法的正确性。

2）时间触发网络拜占庭容错方法能够容忍1个拜占庭故障节点或者2个不一致遗漏故障交换机节点，不能容忍两个及以上并发的拜占庭故障节点。

TTE网络通过COM／MON对能够将危害程度高的拜占庭故障转化为危害程度较低的不一致遗漏故障，提高了时间触发架构的容错能力，降低了容错所需独立路径的个数。本文的结果可以为航空航天高安全等级应用的容错配置提供了更规范的依据。

参考文献（References）

［ 1 ］ Tseng L.Voting in the presence of Byzantine faults［C］ ／／Dependable Computing（PRDC），2017 IEEE 22nd Pacific Rim International Symposium on.IEEE，2017：1-10.

［2］ Zhao W.Byzantine Fault Tolerance［M］.Building Dependable Distributed Systems.John Wiley ＆ Sons， Inc.2014：239-287.

［3］ Rushby J.SAL tutorial： analyzing the fault-tolerant algorithm OM （1）［R］.Computer Science Laboratory， SRI International， Menlo Park， CA， CSL Technical Note， 2004.

［4］ 肖爱斌，杨孟飞，刘波.星载计算节点拜占庭容错设计与验证［J］. 空间控制技术与应用，2008，34（04）：17-22 ＋64.XIAO Aibin， YANG Mengfei， LIU Bo.Design and validation of byzantine fault tolerance for on-board computer［J］.Aerospace Control and Application，2008，34（04）：17-22 ＋ 64.（in Chinese）

［5］ 肖爱斌，胡明明，任宪朝，等.四模冗余拜占庭容错计算节点可靠性分析［J］. 空间控制技术与应用，2014，40（03）：41-46.XIAO Aibin， HU Mingming， Ren Xianchao，etal.Reliability analysis of the computer with quad-modularredundancy Byzantine fault tolerant［ J］.Aerospace Control and Application，2014，40（03）：41-46. （in Chinese）

［6］ 高亚楠，贾英民，蔺玥.基于数据总线的故障容错体系结构的仿真研究［J］. 计算机仿真， 2014（5）：17-21.GAO Yanan， JIA Yingmin， LIN Yue.Simulation study on data bus based fault-tolerant architecture［J］.Computer Simulation， 2014（5）：17-21. （in Chinese）

［7］ 龚健，杨孟飞.一种卫星控制计算节点智能容错方法的探讨［C］／／全国第十三届空间及运动体控制技术学术会议论文集，2008：360-365.Gong Jian，Yang Mengfei.Discussion on intelligent fault tolerance method of satellite control computer［C］ ／／Proceedings of the 13th National Symposium on Space and Vehicle Control Technology，.2008：360-365. （in Chinese）

［8］ Driscoll R.K.， Hall B.Schweiker K.Application Agreement and Integration Services ［R］. NASA／CR-2013-217963，NF1676L-15890.2013

［9］ 孔韵雯，李峭，汤雪乾，等.TTE网络压缩功能计算开销的测量方法［J］. 载人航天，2017，23（05）：645-649.KONG Yunwen， LI Qiao， TANG Xueqian， et al.Measuring method for calculation overhead of compression function in TTE network［J］.Manned Spaceflight， 2017， 23（05）：645-649. （in Chinese）.

［10］ Loveless A T.On TTEthernet for integrated fault-tolerant spacecraft networks［C］ ／／AIAA SPACE 2015 Conference and Exposition.2015.

［11］ SAE AS6802 Time-Triggered Ethernet［S］.SAE，2011.11.

［12］ Loveless A， Fidi C， Wernitznigg S.A proposed byzantine fault-tolerant voting architecture using time-triggered ethernet［R］.JSC-CN-40651，Paper＃2017-01-2111，2017.

［13］ Loveless A.Notional 1FT voting architecturewith time-triggered ethernet［R］.JSC-CN-38812， 2016

［14］ Dutertre B，Easwaran A，Hall B，et al.Model-based analysis of Timed-Triggered Ethernet［C］ ／／IEEE／AIAA， Digital Avionics Systems Conference.IEEE， 2012：9D2-1-9D2-11.

［15］ Rushby J.Bus architectures for safety-critical embedded systems［J］.Lecture Notes in Computer Science， 2001， 2211：306-323.

［16］ 何洋，洪玫，祁琳莹，等.基于模型检测工具NuSMV的功能测试用例生成方法［J］.计算机应用，2015，35（S2）：155-159.HE Yang， HONG Mei， QI Linying， et al.Appoach of functional test case generation based on model checker NuSMV［J］.Computer Applications，2015，35（S2）：155-159.（in Chinese）

［17］ Moura L D， Owre S， Shankar N.The SAL language manual［EB／OL］. （2003）［2017］.http：／／sal.csl.sri.com／doc／language-report.pdf.