-
题名基于TLA+的AFDX冗余管理算法的改进
被引量:1
- 1
-
-
作者
库恒
龙士工
罗昊
-
机构
贵州大学理学院
贵州大学计算机科学与信息学院
-
出处
《计算机工程与设计》
CSCD
北大核心
2013年第3期837-840,853,共5页
-
基金
国家自然科学基金项目(61163001)
贵州省科学技术基金项目(黔科合J字[2012]2135号)
贵州大学自然科学青年科研基金项目(贵大自青基合字(2009)027号)
-
文摘
为了在航空应用中得到更加安全可靠的通讯系统,就目前普遍应用的标准以太网可能会出现的问题,提出了用行为时序逻辑TLA对AFDX冗余管理算法进行形式化分析。在适当的环境中,根据安全性、活性、可用性3个性质,得到两个冗余管理的推论,根据这些性质和推论,提出了3个冗余管理算法,并用TLA+语言进行详细的描述。通过模型检测,表明出RMA13为最优算法。
-
关键词
AFDX冗余管理算法
帧
行为时序逻辑
tla+语言
模型检测
-
Keywords
AFDX redundancy management algorithms
frames
action temporal logic
tla+ language
model checking
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-