Work leading to the Spin verification tool started in 1980.
The first system was called Pan
(short for protocol analyzer)
[H81]. Like Spin, Pan was
a one-pass, on-the-fly, verification system. Unlike
Spin, it was restricted to safety properties.
As far as we can trace back, this was
the first system using on-the-fly verification.
Pan found its first error in a Bell Labs data-switch control
protocol on 21 November 1980.
In 1982, Pan became part of Pandora [H83] (a
verification system built for the Netherlands PTT).
1983 Trace. In 1983 replaced by Trace [H85]. The switch from Pan/Pandora to Trace signalled a change from a verification method based on process algebras [H82] to one that is based on automata. This was originally done for efficiency considerations only, to allow for the construction of a more effective tool. Later, an effective automata based verification theory was developed that justified the switch better still, [VW86].
1987 SuperTrace. In 1987 Trace was replaced with an experimental tool called Supertrace [H88], and in 1988 this experimental tool was integrated into SdlValid [H89] (a verifier for CCITT (now ITU) standard SDL specifications).
1989 Spin. The first version of Spin was written in 1989 to serve as a small example model checking system that could be discussed in a course on protocol verification [H91]. The on-the-fly verification paradigm is now extended in its application to the verification of omega-regular properties in general (including, but not restricted to, linear temporal logic), [H97].
1994 Partial Order Reduction. After many experiments with various reduction methods, Spin was extended in 1994 with a static reduction technique (named STREM, for Static Reduction Method) based on a general theory for partial order reduction [HP94].
1995 LTL conversion. A year later Spin was extended with a builtin algorithm for converting from LTL syntax to automata. The method is based on the algorithm described in [GPVW95].
1997 Minimized Automata. Another significant extension of Spin was the addition of an algorithm for representing the reachable state space with a BDD-like representation that is optimized for application to software verification problems. In software, for instance, one rarely sees as many boolean variables as in hardware. Data is more naturally captured in byte or word-size quantities. Like the partial order reduction technique, the minimized automaton representations can, in some cases, reduce memory requirements exponentially. There is, however, a time penalty for the use of the more compact state representations. The algorithm and its implementation are described in [HP99].
1999 Statement Merging. In version 3.3 of Spin we added a statement merging technique that is more fully explained in [H99]. The technique, though a fairly straightforward extension of partial order reduction rules, can significantly reduce memory use and runtime for the model checker.
2000 Property-based Slicing. The most recent addition to Spin is a property-based slicing technique that can prove beneficial in combination with automated model extraction. More details on this algorithm appear in the lecture notes to the 2000 Summerschool at Marktoberdorf, published by Springer Verlag [H00b].
2003 Support for embedded C code.
Spin Version 4.0 contains direct support for embedded C code fragments,
which offers the required infrastructure for model checking of ANSI-C programs,
through the use of a model extractor [H00a, H03, HJ04].
2007 Support for multicore systems. Spin Version 5.0 contains support for model checking on multicore systems, as detailed in [HB07].
2008 Support for swarm verification. Spin Version 5.1.5 contains support for swarm verification techniques, which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models (see swarm) [HJG08a,HJG08b,HJG10].
2010 Support for Bounded Context Switching.
Spin Version 5.2.5 contains support for bounded context switching,
which can home in on counter-examples with small numbers of unforced
context switches between active processes
2012 Support for Parallel BFS and Priority-based scheduling. Spin Version 6.2.0 contains support for parallelizing the breadth-first search on multicore machines -- with support for the verification of both safety and liveness properties. Also added is a new verification mode to support verification of embedded software, which is often based on priority based scheduling rules. [H12].
|(Page Updated: 10 May 2012)|