| The Model Checker SPIN |
| Posted by: Jones |
5:54pm, Monday, 3 December 2007 |
|
| SPIN is a generic verification system that supports the design and verification of asynchronous process systems. SPIN verification models are focused on proving the correctness of process interactions, and they attempt to abstract as much as possible from internal sequential computations. Process interactions can be specified in SPIN with rendezvous primitives, with asynchronous message passing through buffered channels, through access to shared variables, or with any combination of these. In focusing on asynchronous control in software systems, rather than synchronous control in hardware systems, SPIN distinguishes itself from other well-known approaches to model checking. |
| Gerard Holzmann |
| Appears in IEEE Transactions on Software Engineering |
|
|