论文部分内容阅读
SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.
SpaceWire is a high-speed communication bus standard applied in the field of aeronautics and astronautics, which is of crucial importance in ensuring the reliability and correctness of its design.This paper formalizes the modeling and quantitative analysis of the exchange layer design of SpaceWire by using probabilistic model detection method, Coboff decision-making process (MDP) establishes a formal probability model for the link initialization and normal operation of the exchange layer. The model includes sender, receiver and channel, and extracts four key attributes of the SpaceWire exchange layer, and uses probability calculation tree logic PCTL). The PRISM platform is used to validate and analyze the design of the SpaceWire exchange layer. The probability of packet loss caused by link initialization and the correct transmission of data packets during normal operation is obtained. The quantitative formal analysis For SpaceWire design and implementation can provide a reference.