On the Model Checking of the SpaceWire Link Interface

Wei Hua (Capital Normal University)
Xiaojuan Li (Capital Normal University)
Yong Guan (Capital Normal University)
Zhiping Shi (Capital Normal University)
Jie Zhang (Beijing University of Chemical Technology)
Lingling Dong (Beijing University of Chemical Technology)

Indonesian Journal of Electrical Engineering and Computer Science
Vol 11, No 2: February 2013

In this paper we display a practical approach adopted for the formal verification of SpaceWire using model checking to solve state explosion. SpaceWire is a high-speed, full-duplex serial bus standard which is applied in aerospace, so its functions have a very high accuracy requirements. In order to prove the design of the SpaceWire was faithfully implements the SpaceWire protocol’s specification , we present our experience on the model checking of SpaceWire link interface using the Cadence SMV tool. We applied environment state machine to overcome state explosion and successfully  verified  a number of relevant properties about transmitter and controller of the SpaceWire in reasonable CPU time. DOI: http://dx.doi.org/10.11591/telkomnika.v11i2.2001