SpaceWire协议的形式化建模与概率分析

作者：李月星; 李晓娟; 关永; 王瑞; 张杰; 魏洪兴

来源：小型微型计算机系统, 2013, (09): 2025-2029.

• SpaceWire
• 概率模型检测
• 马尔科夫决策过程
• PRISM SpaceWire
• probabilistic model checking
• Markov decision processes
• PRISM

SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.

• 出版日期2013
• 单位北京化工大学; 首都师范大学; 北京航空航天大学