Formal Verification for SpaceWire Communication Protocol Based on Environment State Machine
Wei Dong Hua, Xiaojuan Li, Yong Guan, Zhiping Shi, Jie Zhang, Lingling Dong · 2012
SpaceWire is a high-speed, full-duplex serial bus standard which is mainly used in the aerospace and other harsh environment, requiring high reliability. The traditional verification methods ,such as simulation and test, are not complete. In this paper, we present our experience on the model checking of data flow control of SpaceWire using the SMV tool. Formal verification is hard to regulate the input variables and some complex properties cannot be directly described with temporal logic, we applied environment state machine and intermediate variables to solve this problem and verify the related properties of the data flow control module, overcoming the incompleteness of the traditional methods.