Formal analysis of a fault tolerant GNC system architecture

In this paper a fault tolerant GNC system architecture is presented, which meets the high reliability requirements of human-rated Spacecraft. This robust GNC architecture with broadcast communications, wraparound technology and fault handling strategy greatly reduces the effects and occurrence of Byzantine disagreement. This paper proposes a formal analysis approach identifying properties of the fault tolerant system, which can be used to avoid design errors at early phases of system development. The simulation results indicate the validity of the fault tolerant system.