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