SpaceWire State Machine Verification Based on Model Checking

Abstract:

SpaceWire is a high-speed data transmission bus standard proposed by ESA for the aerospace applications. Hosted by the National Astronomical Observatories, Chinese Academy of Sciences, the Space Solar Telescope project takes the SpaceWire bus standard as space communication link. The SpaceWire communication circuit implemented by our group is a part of the SST project. In order to improve the fault detection and fault correction capacity and the reliability of the SpaceWire bus, we add a more error analysis and data storage module into the original six state modules of the standard protocol in the exchange layer.We adopt the formal verification method based on the model checking to verify the finite state machine of the SpaceWire control module. The properties expressed by the high-order temporal logic formula are verified automatically to be true by the SMV model verifier of the Cadence Company. Verification results show that our SpaceWire bus implementation and the additional error analysis and data storage module are faithful to the protocol specification. Therefore, we also can integrate SpaceWire bus circuit into the SST project.

• Periodical: Applied Mechanics and Materials (Volumes 55-57)
• Pages: 2192-2196
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.55-57.2192
• Online since: May 2011
• Authors: Zhi Quan Dai, Yong Guan, Sheng Zhen Jin, Zhi Ping Shi, Xiao Juan Li, Jie Zhang
• Keywords: Communication Bus, Formal Verification, High-Order Temporal Logic, Model Checking, Reliability

References

[1] European Cooperation for Space Standardization, Space engineering. SpaceWire - links, nodes, routers, and networks, (ECSS-E-50-12A), http: /www. ecss. nl/forums/ecss/dispatch. cgi/ standards/showFile/100302/d20090722143301/No/ECSS-E-50-12A(24January2003). pdf(2003).

DOI: 10.2514/6.1996-4305

[2] Jungang Han and Huimin Du, in: Formal Verification of Digital Hardware. Peking University Press(2001).

[3] Fei Yin, Formal Verification Method, Electronic Computer, Vol. 24-28 (2002), p.154.

[4] E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press(2000).

[5] Christel Baier and Joost-Pieter Katoen, Principles of model checking, MIT Press(2008).

DOI: 10.1093/comjnl/bxp025

[6] K.L. McMillan, SMV Reference Manual, Cadence Berkeley Labs, Berkeley(2002).

[7] Kaile Su, Yuxiang Luo, Guanfeng Lv, Symbolic model checking CTL*, Chinese Journal of Computers(2005), 28 Volume XI.

[8] K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers(1992).

[9] Sanjit A. Seshia, Wenchao Li, Subhasish Mitra. Verification-guided soft error resilience, Design, Automation, and Test in Europe(2007), Pages: 1442 – 1447.

DOI: 10.1109/date.2007.364501

[10] Tomáš Kratochvíla, Vojtěch Řehák, Pavel Šimeček, Verification of COMBO6 VHDL Design, CESNET(2003).