The Future of Testing Tools (Continued)

FTPOnline: Who should use SPIN?

Gerard Holzmann: One of the more appealing things about the SPIN tool is that it can be used by requirements engineers, system designers, software developers, and by testers. The types of analysis that are supported by this tool can be used before any code has been written, precisely because it can work with higher-level design sketches. A good argument can be made that this is in fact the best place to use the tool.

In practice, though, SPIN is often used after the code for an application has been written, when the classical approaches to software testing are seen to fall short. Since the tool is freely available (from http://spinroot.com) for both commercial and non-commercial use, it requires no great investment, other than a mild learning curve in the use of the tool and the specification language that it supports.

FTPOnline: Can you give examples of applications where SPIN made a major difference?

Gerard Holzmann: There have been many applications of this tool, but a few really stand out. At Lucent Technologies we used SPIN over a period of two years to check that the call-processing software for a new telephone switch was free of concurrency-related bugs. The code was heavily multi-threaded, as most applications are these days. The call processing code was also considered to be the most difficult part of the switch to get right: it really forms the heart of the switch.

We were able to check the code very thoroughly at implementation level (the code was written in C). To do so, we relied on a relatively new feature in SPIN that allows the use of embedded C code within the verification models. Towards the end of the product development cycle for the Lucent switch, we were able to check the call-processing code for compliance with over 200 logical and functional properties in about 40 minutes of CPU time.

During the lifetime of this product, not a single software defect was reported in this part of the code: a highly unusual phenomenon, and a testament to the effectiveness of the SPIN-based approach to testing. Today, SPIN tends to be used mostly for critical software development, and more sporadically in routine software development. At NASA/JPL, for instance, SPIN is used to check that the critical components of flight software for space missions are bug-free.

We estimate that there are between 5,000 and 10,000 people who routinely use the SPIN tool today. The potential number of users for SPIN runs in the hundreds of thousands, though, so we have more work to do.