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

• 作者: 库恒 罗昊 龙士工
• 来源期刊: 计算机工程与设计
• 学科: 工学
• 关键词: AFDX冗余管理算法 帧 行为时序逻辑 TLA+语言 模型检测
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 信息安全技术
• 页码范围: 837-840,853
• 页数: 5页
• 分类号: TP301.2
• 字数: 4179字
• 语种: 中文

摘要

为了在航空应用中得到更加安全可靠的通讯系统,就目前普遍应用的标准以太网可能会出现的问题,提出了用行为时序逻辑TLA对AFDX冗余管理算法进行形式化分析.在适当的环境中,根据安全性、活性、可用性3个性质,得到两个冗余管理的推论,根据这些性质和推论,提出了3个冗余管理算法,并用TLA+语言进行详细的描述.通过模型检测,表明出RMA13为最优算法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗昊	贵州大学计算机科学与信息学院	4	6	2.0	2.0
2	龙士工	贵州大学计算机科学与信息学院	39	110	5.0	9.0
3	库恒	贵州大学理学院	2	4	2.0	2.0