Spin uses a high level language called PROMELA to describe specifications. Given a PROMELA program, it can interactively simulate the system's execution or generate a C program that performs a fast exhaustive verification of the system's state space. It reports on deadlocks, race conditions, unexecutable code, incorrect system invariants, and other logical design errors. Spin's intended purpose is to verify correctness rather than security, but many of the concepts, especially the ability to detect race conditions, may be useful in building code checking tools.

URL: http://netlib.bell-labs.com/netlib/spin/whatispin.html

Spin runs on both Unix and Windows platforms.

Pros

• It's open source.
• It is widely distributed (over 2,500 users est.), and highly respected.

• It requires a description of a system to be written in PROMELA before it can be used.

Classification:
Static vs. Dynamic: Static
Library vs. Instrumenting: Instrumenting
Testing vs. Production: Testing
Opaque vs. Clear: Clear
List vs. Heuristic: Heuristic
Conservative vs. Liberal: Conservative
Concurrent vs. Single Program: Single Program
Alert vs. Fix: Alert

Evaluated by Homer Briggs on 8/21/2000