摘要
SpaceWire总线作为航天器数据/控制的"神经中枢",其网络层的结构和应用设计是系统可靠性的重要影响因素.为了在SpaceWire总线网络层设计部署过程中,对其进行形式化分析,发现设计缺陷,提高可靠性.提出了一个用于SpaceWire网络层验证的形式化分析模板框架,将网络层的核心要素:实时数据包、终端节点、路由器和路由机制都使用时间自动机建模.然后根据具体案例将之实例化,并在UPPAAL模型检验工具中根据规范提出性质进行检验.典型案例的分析验证了所提出的方法的有效性.
As the "nerve center"of spacecraft data/control,SpaeWire structure and application design of its network layer are important influencing factors of system reliability.In the process of designing and deploying SpaceWire network,in order to analyze it formally,find defects and improve the reliability,a formal analysis template framework for SpaceWire network layer analysis is proposed.All the components of the network layer:real-time packet,terminal node,router and routing mechanism are modeled as timed automata.Then a simplified case is built in the UPPAAL model checking tool,and the extraction property is verified.The analysis of typical cases verifies the effectiveness of the proposed method.
作者
潘雄
邓威
苑政国
PAN Xiong;DENG Wei;YUAN Zheng-guo(Institute of Optics and Electronics,Beihang University,Beijing 100083,China)
出处
《微电子学与计算机》
北大核心
2019年第1期1-5,共5页
Microelectronics & Computer
