SpaceWire网络层分析的时间自动机模型
|
摘要
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.
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.
引文
[1] European Space Agency.SpaceWire-home[EB/OL].[2018-01-19].http://www.spacewire.esa.int/content/Home/HomeIntro.php,2017.
[2]侯剑儒.SpaceWire重要特性与仿真研究[D].北京:中国科学院大学,2013.
[3]李黎明,关永,吴敏华,等.运用定理证明的形式化方法验证SpaceWire编码电路[J].小型微型计算机系统,2012,33(6):1372-1376.
[4]张玉鹏,施智平,关永,等.SpaceWire译码电路在HOL4中的形式化验证[J].小型微型计算机系统,2013,34(8):1959-1963.
[5]李艳春,李晓娟,关永,等.基于xMAS模型的SpaceWire信誉逻辑的形式化验证[J].计算机科学,2016,43(2):113-117.
[6]董玲玲,关永,李晓娟,等.用LTL模型检验的方法验证SpaceWire检错机制[J].计算机工程与应用,2012,48(22):88-94.
[7]李月星,李晓娟,关永,等.SpaceWire协议的形式化建模与概率分析[J].小型微型计算机系统,2013,34(9):2025-2029.
[8]金仙力,孙国梓,杨庚.基于层次时间自动机的动态行为取证建模方法[J].微电子学与计算机,2012,29(11):18-21.
[2]侯剑儒.SpaceWire重要特性与仿真研究[D].北京:中国科学院大学,2013.
[3]李黎明,关永,吴敏华,等.运用定理证明的形式化方法验证SpaceWire编码电路[J].小型微型计算机系统,2012,33(6):1372-1376.
[4]张玉鹏,施智平,关永,等.SpaceWire译码电路在HOL4中的形式化验证[J].小型微型计算机系统,2013,34(8):1959-1963.
[5]李艳春,李晓娟,关永,等.基于xMAS模型的SpaceWire信誉逻辑的形式化验证[J].计算机科学,2016,43(2):113-117.
[6]董玲玲,关永,李晓娟,等.用LTL模型检验的方法验证SpaceWire检错机制[J].计算机工程与应用,2012,48(22):88-94.
[7]李月星,李晓娟,关永,等.SpaceWire协议的形式化建模与概率分析[J].小型微型计算机系统,2013,34(9):2025-2029.
[8]金仙力,孙国梓,杨庚.基于层次时间自动机的动态行为取证建模方法[J].微电子学与计算机,2012,29(11):18-21.