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

Formal Modeling and Probabilistic Analysis of SpaceWire Protocol

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.