O. S. Matlin, E. Lusk, and W. McCune, "SPINning Parallel Systems Software," 9th International SPIN Workshop, Lecture Notes in Computer Science, Springer, vol. 2318, Grenoble, France, 2002, 1969, pp. 213-220, . [pdf]
We describe our experiences in using Spin to verify parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of processes connected by Unix network sockets. Its dynamic nature is easily expressible in the Spin/Promela framework but poses performance and scalability challenges. We present here the results of expressing some of the parallel algorithms of MPD and executing verification runs with Spin.