Abstract: SpaceWire protocol is a high-speed communication bus protocol applied to aerospace,so it is very important for communication system to ensure the reliability of the design.Due to the presence of a large number of queues,distributed control and concurrency,the traditional verification methods have incomplete defects and state explosion when model checking occurs.This paper presented a formal verification method of credit logic in SpaceWire communication system with xMAS model.xMAS model retains the structural information in lower level and can verify high-level attri-butes.The paper built an abstract xMAS model for credit logic and listed three key properties including sending,receiving and data consistency.Correctness of the properties was verified automatically by the ACL2 theorem proving tool.It can provide effective reference for system design under the guidance of verification.

Key words: xMAS model,Credit logic,SpaceWire,Formal verification,ACL2