Formalization and Verification of Go-based New Simple Queue System

NSQ (New Simple Queue) is a real-time distributed messaging platform implemented by Go language. It’s designed to operate at scale stably and efficiently handle billions of messages per day. Its decentralized topology guarantees fault tolerance, high availability, and reliable message delivery. Operationally, NSQ is elastic to configure and deploy. With the broad application of the NSQ message system, its security and stability have attracted extensive concentration. Therefore, it is crucial to conduct a rigorous analysis and verification of NSQ’s properties. In this paper, we employ process algebra CSP (Communicating Sequential Processes) to model the core functional modules of the NSQ. In addition, we utilize the model checker PAT (Process Analysis Toolkit) to verify five properties of the model, including divergence freedom, reachability, scalability, availability, and flow controllability. The verification results demonstrate that the NSQ system satisfies all the above properties, proving that the system has high flexibility and robustness while providing credible and efficient message delivery.