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

作     者：李月星 李晓娟 关永 王瑞 张杰 魏洪兴 LI Yue-xing;LI Xiao-juan;GUAN Yong;WANG Rui;ZHANG Jie;WEI Hong-xing

作者机构：高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室首都师范大学信息工程学院北京100048 北京化工大学信息科学与技术学院北京100029 北京航空航天大学机械工程及自动化学院北京100191 

基　　金：国际科技合作计划项目(2011DFG13000)资助 北京市自然科学基金暨北京教委重点项目(4122017 KZ201210028036)资助 国家自然科学基金项目(61070049 61170304 61104035)资助 

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2013年第34卷第9期

页      码：2025-2029页

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

主 题 词：SpaceWire 概率模型检测 马尔科夫决策过程 PRISM 

学科分类：08[工学] 0839[0839] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-1220.2013.09.012

馆 藏 号：203219342...