Model Checking for SpaceWire Link Interface Design Using Uppaal

SpaceWire provides a full-duplex, point-to-point, serial data communication network for on-board applications. This paper presents a Timed Automata approach to modeling, analyzing, and verifying the SpaceWire link interface design. A network of Timed Automata is established to formalize the link interface, including Controller, Transmitter, Receiver, and Channel. Uppaal, a Timed Automata based model checker for real-time system, is adopted for symbolic verification of SpaceWire. The SpaceWire specification requirements are formulated in computational tree logic (CTL). In this way, we have the high-level models of both link ends interacted and verified resorting to Uppaal. It is demonstrated that link initialization can be made successfully within the time scheduled by the requirements of SpaceWire. Furthermore, the paper presents the time properties of the model and makes an analysis of time limitation in the situation that disconnection error occurs.