http://spinroot.com/spin/Man/Quick.html
says:
Spin is a tool for analyzing the logical consistency of distributed systems, specifically of data communication protocols. The system is described in a modeling language called Promela (Process or Protocol Meta Language). The language allows for the dynamic creation of concurrent processes. Communication via message channels can be defined to be synchronous (i.e., rendez-vous), or asynchronous (i.e., buffered). Xspin is a graphical front-end to drive Spin (written in Tcl/Tk).@since Metropolis-1.0