|
General Description
Some of the features that set Spin apart from
related verification systems are:
-
Spin targets the efficient verification of multi-threaded software,
not the verification of hardware circuits. The tool supports a high level
language to specify systems descriptions called PROMELA
(short for: PROcess MEta LAnguage).
Spin has been used to trace logical design errors in
distributed systems design, such as operating systems,
data communications protocols, switching systems,
concurrent algorithms, railway signaling protocols, control
software for spacecraft, nuclear power plants, etc.
The tool checks the logical consistency of a specification and
reports on deadlocks, race conditions, different types of
incompleteness, and unwarranted
assumptions about the relative speeds of processes.
-
Spin provides direct support for
the use of embedded C code as part of model specifications.
This makes it possible to directly verify implementation
level software specifications, using Spin as a driver and
as a logic engine to verify high level temporal properties.
With the help of the model extractor modex
it is also possible to mechanically derive a PROMELA
model from concurrent C code, and verify it with Spin.
-
Spin provides direct support for
the use of multi-core computers for model checking
runs - supporting the verification of both safety and liveness properties.
-
Spin works on-the-fly, which means that it
avoids the need to preconstruct a global state graph, or
Kripke structure, as a prerequisite for the verification of
system properties. This makes it possible to verify very large system models.
-
Spin can be used as a full LTL model checking system, supporting all
correctness requirements expressible in linear time temporal logic,
but it can also be used as an efficient on-the-fly verifier for more
basic safety and liveness properties. Many of the latter properties
can be expressed, and verified, without the use of LTL.
Correctness properties can be specified as system
or process invariants (using assertions), as
linear temporal logic requirements (LTL), as formal
Büchi automata, or more broadly as general
omega-regular properties in the syntax of Spin never claims.
-
The tool is one of very few verification tools that supports dynamically
growing and shrinking numbers of processes, using a
rubber state vector technique.
-
The tool supports both rendezvous and buffered
message passing, and communication through shared memory.
Mixed systems, using both synchronous and asynchronous communications,
are also supported. Message channel identifiers for both rendezvous
and buffered channels, can be passed from
one process to another in messages, which makes it possible (for instance)
to verify models from mobile pi-calculus.
-
The tool supports random, interactive and guided
simulation, and both exhaustive and partial proof techniques,
based on depth-first search, breadth-first search, or bounded context-switching.
The tool is designed to scale well, and to
handle large problem sizes efficiently.
-
To optimize verification runs, Spin exploits efficient
partial order reduction techniques, and (optionally) BDD-like
state storage techniques.
To verify a design, a formal model is built using
PROMELA, Spin's input language.
PROMELA is a non-deterministic
language, loosely based on Dijkstra's guarded command
language notation and borrowing the notation
for I/O operations from Hoare's CSP language.
Main Usage Modes
Spin can be used in four main modes:
-
as a simulator, allowing for rapid prototyping
with a random, guided, or interactive simulations
-
as an exhaustive verifier,
capable of rigorously proving the validity of
user specified correctness requirements
(using partial order reduction theory
to optimize the search)
-
as proof approximation system that can
validate even very large system models
with maximal coverage of the state space.
-
as a driver for
swarm verification
(a new form of swarm computing that can exploit cloud networks
of arbitrary size), 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.
All Spin software is written in ISO-standard C,
and is portable across all versions of Unix, Linux,
cygwin, Plan9, Inferno, Solaris, Mac, and Windows.
| |