The Future of Testing Tools (Continued)

FTPOnline: Where can we learn more?

Gerard Holzmann: Since the ACM award, SPIN received a lot of attention and has attracted significantly more users. This has led to the publication of a new book that gives a comprehensive overview of how the tool works, and how it can be used. The book, called The SPIN Model Checker: Primer and Reference Manual, was published by Addison-Wesley.

A good place to find out more about the tool and its applications is also the annual SPIN workshop, which has been held since 1995. It is supported by ACM SIGSOFT.

FTPOnline: You wrote an article as part of FTP's "Future of Software" report in late 2000. In it, you predicted embedded smart-source code analyzers warning developers immediately of subtle bugs as they get introduced. How close is SPIN Version 4 to that prediction?

Gerard Holzmann: This is indeed my long-term goal, to turn this prediction into reality. SPIN is known today as one of the most efficient and powerful checkers for multi-threaded software systems. To achieve this level of efficiency, the tool employs search algorithms that are founded on many decades of research in automata theory, logic, and graph theory. Every few years we see another major leap forward when a new type of algorithm is discovered that can reduce runtime and memory use of the tool still further.

It is always dangerous to extrapolate, but if we can continue this trend, it should be possible to deliver on this promise. Within about 5 to 10 years we should have been able to refine this technology to the point where it can be made invisible, and can be "hidden" in a standard language compiler.