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

作者:潘雄; 邓威*; 苑政国
来源:微电子学与计算机, 2019, 36(01): 1-5.
DOI:10.19304/j.cnki.issn1000-7180.2019.01.001

摘要

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

全文