TY - GEN
T1 - Model checking for spacewire link interface design using uppaal
AU - Luo, Ping
AU - Wang, Rui
AU - Li, Xiaojuan
AU - Guan, Yong
AU - Wei, Hongxing
AU - Zhang, Jie
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - SpaceWire
KW - Uppaal
KW - model checking
KW - timed automata
UR - https://www.scopus.com/pages/publications/84885617412
U2 - 10.1109/COMPSACW.2013.56
DO - 10.1109/COMPSACW.2013.56
M3 - 会议稿件
AN - SCOPUS:84885617412
SN - 9780769549873
T3 - Proceedings - International Computer Software and Applications Conference
SP - 181
EP - 186
BT - Proceedings - 2013 IEEE 37th Annual Computer Software and Applications Conference Workshops, COMPSACW 2013
PB - IEEE Computer Society
T2 - 37th Annual IEEE Computer Software and Applications Conference Workshops, COMPSACW 2013
Y2 - 22 July 2013 through 26 July 2013
ER -