基于TLA+的AFDX冗余管理算法的改进

摘要

To get more safety and reliable communications system, according to standard Ethernet of the current widespread application maybe occur problems, the formal analysis of AFDX redundancy management algorithms is put forward based on TLA In the appropriate environment, based on three properties of safety, Iiveness, availability, two deduction of redundancy management are obtained, and based on these properties and deductions, three redundancy management algorithms, and detailed description based on TLA+ language are presented. At last, through the model checking the result, proof to RMA13 is the best of algorithms.%为了在航空应用中得到更加安全可靠的通讯系统,就目前普遍应用的标准以太网可能会出现的问题,提出了用行为时序逻辑TLA对AFDX冗余管理算法进行形式化分析.在适当的环境中,根据安全性、活性、可用性3个性质,得到两个冗余管理的推论,根据这些性质和推论,提出了3个冗余管理算法,并用TLA+语言进行详细的描述.通过模型检测,表明出RMA13为最优算法.