On the Model Checking of the SpaceWire Link Interface

Wei Hua, Xiaojuan Li, Yong Guan, Zhiping Shi, Jie Zhang, Lingling Dong

Abstract


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


Full Text:

PDF

Refbacks

  • There are currently no refbacks.


Creative Commons License
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

Indonesian Journal of Electrical Engineering and Computer Science (IJEECS)
p-ISSN: 2502-4752, e-ISSN: 2502-4760
This journal is published by the Institute of Advanced Engineering and Science (IAES) in collaboration with Intelektual Pustaka Media Utama (IPMU).

shopify stats IJEECS visitor statistics