SpaceWire网络层分析的时间自动机模型

摘要

SpaceWire总线作为航天器数据/控制的"神经中枢",其网络层的结构和应用设计是系统可靠性的重要影响因素.为了在SpaceWire总线网络层设计部署过程中,对其进行形式化分析,发现设计缺陷,提高可靠性.提出了一个用于SpaceWire网络层验证的形式化分析模板框架,将网络层的核心要素:实时数据包、终端节点、路由器和路由机制都使用时间自动机建模.然后根据具体案例将之实例化,并在UPPAAL模型检验工具中根据规范提出性质进行检验.典型案例的分析验证了所提出的方法的有效性.