Analysis of distributed spin applied to industrial-scale models

As software systems become increasingly complex, there is growing interest in the use of formal techniques to obtain higher assurance in their correctness. The most commonly used tools involve model-checking, such as SMV and Spin. But modeling complex systems with a high degree of fidelity implies exceedingly large state spaces that must be analyzed. These state spaces are typically too large for single processing nodes, in spite of great advances in memory reduction techniques. Moreover, approximation techniques such as hash compaction are less well-received where safety-critical systems are concerned. Effective distribution of the problem over many processing nodes has the potential of supporting the huge state spaces. Since our primary interest is in safety-critical software, we have spent considerable time evaluating the performance of distributed implementations of Spin in this context. In this paper, we present our analysis of PSPIN, a distributed implementation of Spin. We identify key measures of effectiveness, and evaluate PSPIN with respect to these measures. We also present an alternative approach to partitioning that performs comparably with respect to all measures, and is up to orders of magnitude faster. Finally, we consider the question of which measures have the greatest impact on peak memory, a measure that is most critical to effective distribution.