Property Specification in SPIN: SPIN allows specification of assertions, which check a predicate of a state at a point in an execution, and also allows for specification of progress properties (e.g., no starvation) by allowing statements to be labeled as progress states. A report is generated if there are infinite executions that do not pass through one of these marked states. SPIN also provides a facility for stating never claims, behavior that should never occur. Never claims are checked at each step in the execution. This allows you to state an invariant (which may even be a path property) that should never be violated. You can specify temporal properties using a timeline editor.
Linear Temporal Logic (LTL) is a language to express properties that hold for paths throughout the state space. The SPIN model checker allows temporal properties to be expressed in this language; the properties are then compiled into never claims. Formulas in LTL are built of state properties and the following operators: [] (always), <> (eventually), and U (until), plus the standard logical operators. The semantics is as follows:
- P: The property P holds in the current state.
- []P: The property P holds in this state and in all future states.
- <>P: The property P eventually holds in this or a future state.
- P U Q: The property P holds in this state and future states until a state is reached where the property Q holds.