Analysis of SpaceWire Link Initialization Time based on Timed Automata
Download as PDF
DOI: 10.23977/meet.2019.93740
Author(s)
Ping Luo, Daiwu Chen, Dong Xie, Yan Zhang
Corresponding Author
Ping Luo
ABSTRACT
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.
KEYWORDS
Spacewire,Timed Automata,Model Checking