Education, Science, Technology, Innovation and Life
Open Access
Sign In

Analysis of SpaceWire Link Initialization Time based on Timed Automata

Download as PDF

DOI: 10.23977/meet.2019.93740


Ping Luo, Daiwu Chen, Dong Xie, Yan Zhang

Corresponding Author

Ping Luo


SpaceWire provides a full-duplex, bidirectional, point-to-point, high speed data link for on-board network. It is significant to make sure of the link connection successfully and reliably. Based on timed automata, the paper presents the modeling of the modules of Controller, Timer, Transmitter and Receiver implemented in SpaceWire link interface, and the simulation of the link initialization. The tool we adopted is Uppaal, a timed automata based model checker for real-time system. In Uppaal, we analyzed some time properties during the link initialization process. It turned out that there were details of the implementation inconsistent with the SpaceWire protocol standard. The state machine of the Controller for the link interface didn’t wait enough time in some states as expected. Finally, we found out the reason caused the problem and revised the implementation.


Spacewire,Timed Automata,Model Checking

All published work is licensed under a Creative Commons Attribution 4.0 International License.

Copyright © 2016 - 2031 Clausius Scientific Press Inc. All Rights Reserved.