1e42cfef2b
Spin is an efficient on-the-fly verification system (a `model checker') for asynchronous concurrent systems, such as data communication protocols, distributed operating systems, database systems, etc. It can be used to prove both safety and liveness properties, including all correctness requirements expressible in linear time temporal logic. Spin uses a high level language to specify systems descriptions, called PROMELA (PROcess MEta LAnguage).
9 lines
449 B
Text
9 lines
449 B
Text
Spin is an efficient on-the-fly verification system
|
|
(a `model checker') for asynchronous concurrent systems,
|
|
such as data communication protocols, distributed operating
|
|
systems, database systems, etc.
|
|
It can be used to prove both safety and liveness properties,
|
|
including all correctness requirements expressible in linear
|
|
time temporal logic.
|
|
Spin uses a high level language to specify systems descriptions,
|
|
called PROMELA (PROcess MEta LAnguage).
|