摘要
SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.
SpaceWire is a bus standard for high speed data transmission in aerospace. It is very important to guarantee the reliability and correctness of the design. This paper harnesses probabilistic model checking to build formal model and make quantitative formal analysis for the design of SpaceWire's exchange level. The paper builds formal probabilistic models for the process of link initializa- tion and normal operation of the exchange level based on MDP (Markov Decision Process}. The sender, the receiver and the channel are included in the models. The paper extracts four key properties of the exchange level of SpaceWire. The properties are described in PCTL (Probabilistic Computation Tree Logic ). The design of SpaceWire's exchange level is verified and analyzed by the PRISM platform. When the probability of losing packet is different, the paper gets the probability of the successful initialization, and the prob- ability of correct packets transmission during normal operation. The quantitative verification results provide a useful reference for the design and implementation of SpaceWire.
出处
《小型微型计算机系统》
CSCD
北大核心
2013年第9期2025-2029,共5页
Journal of Chinese Computer Systems
基金
国际科技合作计划项目(2011DFG13000)资助
北京市自然科学基金暨北京教委重点项目(4122017
KZ201210028036)资助
国家自然科学基金项目(61070049
61170304
61104035)资助