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

• 作者: 关永 张杰 李晓娟 李月星 王瑞 魏洪兴
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: SpaceWire 概率模型检测 马尔科夫决策过程 PRISM
• 年，卷（期）: 2013,（9）
• 所属期刊栏目: 计算机网络与通信技术
• 页码范围: 2025-2029
• 页数: 5页
• 分类号: TP309
• 字数: 3982字
• 语种: 中文

摘要

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