一种拜占庭容错体系结构的形式化分析

摘要

针对特殊任务航天器的高可靠性和高安全性要求,提出了一种基于并行通道配合计算机交联(Computer Cross Talk)的导航制导与控制分系统(GNC分系统)体系结构.该体系结构使用1553B数据总线和TTP(Time Triggered Protocol)数据总线,配合拜占庭交联模式的GNC控制器,通过数据交换和数据比对满足系统故障检测和故障容错的要求.使用SCADE系统设计工具软件对该系统进行正常情况和故障情况建模,并对系统的故障容错特性进行形式化验证,验证结果表明,系统可以容忍任意一重故障且不损失任何性能,并具备实时现场恢复的能力。