Formal Verification for SpaceWire Communication Protocol Based on Environment State Machine

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.