The Future of Testing Tools (Continued)

FTPOnline: How does one use SPIN?

Gerard Holzmann: SPIN works somewhat differently from a regular testing tool. The SPIN user is asked to create a relatively precise description of an algorithm as an executable model. The model can be simulated in various ways, which makes SPIN an excellent rapid-prototyping tool. But the big thing is that each SPIN model can also be verified thoroughly. A SPIN model is typically defined at a slightly higher level than the implementation, to avoid having to include also more trusted, routine parts of an application (like the precise implementation of process scheduling, message passing, or memory management).

Ideally, the level at which this executable model is defined matches the level of a white-board sketch that a developer would use to explain the essence of the working of a system to a peer (and why he believes that it will all work correctly). SPIN can take that description and then thoroughly analyze the behavior that was specified to see if certain types of concurrency-related errors can or cannot occur. It typically takes no more than an hour or so to build a SPIN model, and it usually takes no more than a few seconds for SPIN to show where the bugs are.

Running SPIN for the first time is usually an eye-opener for a new user. SPIN will virtually instantaneously identify possible sequences of behavior that the user never imagined would be possible: precisely the types of behavior that can strike in practice and either greatly annoy the end-customer, or cause inestimable damage by hanging the system or by corrupting data in mysterious ways.

SPIN is powerful enough that it is also possible to define very detailed models of concurrent systems behavior, down to the level of implementation-level code. The analyses can become more compute-intensive if the level of the model is too detailed, though, so there is a benefit in sticking with slightly more general SPIN models. The benefit of a more general model is that the results of an analysis apply immediately to a broader class of possible implementations: the analysis also becomes more generally applicable to a class of possible designs.