Modeling and Analysis of SpaceWire Network Based on Timed Automata

PAN Xiong; DENG Wei; YUAN Zheng-guo

Chinese

您当前的位置：

首页 >

文章列表页 >

Modeling and Analysis of SpaceWire Network Based on Timed Automata

更新时间：2026-09-04

- Modeling and Analysis of SpaceWire Network Based on Timed Automata
- Vol. 36, Issue 1, Pages: 1-5(2019)
- 作者机构：
  
  北京航空航天大学光电技术研究所,北京,100083
- 作者简介：
- 基金信息：
- DOI：
  CLC：
- Published：2019
- 稿件说明：
移动端阅览
潘雄, 邓威, 苑政国. SpaceWire网络层分析的时间自动机模型[J]. 微电子学与计算机, 2019, 36(1): 1-5.

PAN Xiong, DENG Wei, YUAN Zheng-guo. Modeling and Analysis of SpaceWire Network Based on Timed Automata[J]. 2019, 36(1): 1-5.
潘雄, 邓威, 苑政国. SpaceWire网络层分析的时间自动机模型[J]. 微电子学与计算机, 2019, 36(1): 1-5. DOI：

PAN Xiong, DENG Wei, YUAN Zheng-guo. Modeling and Analysis of SpaceWire Network Based on Timed Automata[J]. 2019, 36(1): 1-5. DOI：

摘要

SpaceWire总线作为航天器数据/控制的"神经中枢"

其网络层的结构和应用设计是系统可靠性的重要影响因素.为了在SpaceWire总线网络层设计部署过程中

对其进行形式化分析

发现设计缺陷

提高可靠性.提出了一个用于SpaceWire网络层验证的形式化分析模板框架

将网络层的核心要素:实时数据包、终端节点、路由器和路由机制都使用时间自动机建模.然后根据具体案例将之实例化

并在UPPAAL模型检验工具中根据规范提出性质进行检验.典型案例的分析验证了所提出的方法的有效性.

Abstract

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.

关键词

Keywords

references

侯剑儒. SpaceWire重要特性与仿真研究[D].北京: 中国科学院大学, 2013.

李艳春, 李晓娟, 关永, 等.基于xMAS模型的SpaceWire信誉逻辑的形式化验证[J].计算机科学, 2016, 43(2):113-117. DOI: 113

李黎明, 关永, 吴敏华, 等.运用定理证明的形式化方法验证SpaceWire编码电路[J].小型微型计算机系统, 2012, 33(6):1372-1376. DOI: 1372

张玉鹏, 施智平, 关永, 等. SpaceWire译码电路在HOL4中的形式化验证[J].小型微型计算机系统, 2013, 34(8):1959-1963. DOI: 1959

李月星, 李晓娟, 关永, 等. SpaceWire协议的形式化建模与概率分析[J].小型微型计算机系统, 2013, 34(9):2025-2029. DOI: 2025

金仙力, 孙国梓, 杨庚.基于层次时间自动机的动态行为取证建模方法[J].微电子学与计算机, 2012, 29(11):18-21. DOI: 18

董玲玲, 关永, 李晓娟, 等.用LTL模型检验的方法验证SpaceWire检错机制[J].计算机工程与应用, 2012, 48(22):88-94. DOI: 88

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on High Confidence Level Bit Error Eate Measurement of Space Wire

High gain stability high temperature operational amplifier based on reverse body bias

A review of large model development: technological evolution from BERT to Deepseek

Steganography model guided by attention mechanism and improved dense convolution

Monte carlo analysis of V-layout trench SiC neutron detector

Related Author

CHEN Wei-guo

LIU Huan

WANG Jian-feng

WU Long-sheng

Related Institution

Xi'an Microelectronics Technology Institute

AI问答

Postal code：100079
Tel：（010）53879206 Email：tmw@bjxintong.com.cn
Technical support is provided by Beijing Founder electronics co., LTD 京ICP备09082226号-64 京公网安备11010602201714号
It is recommended to read the content of this site in Chrome&IE9+. Please switch to extreme mode in browser 360.
Cookies We use cookies to help provide and enhance our service and tailor content. By continuing, you agree to the use of cookies.

⁰