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

摘要

对于时间触发以太网的拜占庭容错方法,已有的推理性论证表明网络的分布式时钟同步机制有利于容错过程中实现交互一致性.为对该容错方法的正确性进行严格验证,进一步采用模型检查的形式化分析手段,通过符号分析实验室(SAL)形式化工具,构建了网络节点模型,建立了时间触发体系结构下的拜占庭容错场景,设定了容错操作活性、一致性和有效性等属性的形式化定理.模型检查的结果表明:在三冗余独立路径条件下,该方法可以容忍一个拜占庭故障,且在存在指令/监视对(COM/MON pair)的条件下可以容忍2个高完整性配置节点的"不一致遗漏"故障.与推理论证手段相比,SAL模型检查为时间触发交换式网络在航空航天高安全关键等级系统中的容错配置提供了更规范的依据.%Existed reasoning proof indicates that distributed clock synchronization mechanism con-tributes to achieving interactive agreement during fault-tolerant process for the Byzantine fault-toler-ant method of the Time-Triggered Ethernet. The correctness of this fault-tolerant method was further strictly verified by the model-checking formal analysis tool. After the network node modules were built,the Byzantine fault tolerance scenarios were established by the SAL(Symbolic Analysis Labo-ratory)formal analysis tool in the Time-Triggered Architecture. The formal theorems of the attribu-tion such as liveness, agreement and validity were specified. The results showed that this method could tolerate a Byzantine fault node under three independent paths. And it could also tolerate in-consistent-omission faults of two high-integrity nodes with each node configured Commander/Monitor (COM/MON)pair. Comparing to the reasoning proof, model-checking based on SAL presented more normal evidence for the fault tolerance configuration of the Time-Triggered switched network in the aeronautical and space high safety-critical level systems.