0.5 Using temporal logic to specify properties

So far, we've seen some of the built-in checks performed by SPIN: assertions, deadlock, non-progress, and one notion of fairness.But what about other properties we'd like to check for? We might be interested in properties which the implementors ofour particular tool weren't interested in, or hadn't thought of. Fortunately, SPIN does includea general property-checking mechanism: If we can state our property in a particularformal temporal logic , then SPIN will allow us to check the property.

First, we'll introduce the syntax and semantics of one particular temporal logic, LTL . Then , we'll return we'll return to SPIN and howit uses temporal logic for verification.

First, we reflect that some propertiessafety propertiescan be phrased in terms of ``some particular state is unreachable''.For example, a state where two processes are sending information to the printer simultaneously never occurs.Failed assertions can be viewed as a transition to a fail-state, and we require that this state is unreachable.Deadlock can be viewed as a state with no legal outgoing transition, and not all processes sitting in an end-state.

Similarly we reflect that other propertiesliveness propertiesare about entire traces, not just some state in a trace. For instance, non-progress cycles is a cycle which does not containany states labeled as progress states.

We want a richer language to have a way of talking about traces, but that is precise and not subject to English's vagaries.We'll work towards using logica temporal logic specifically designed to beconducive to expressing concepts which arise in concurrent programming. But before we can even do that, we need a clear model ofconcurrent programs, and more formal definitions of some ideas we've already seen.

Concurrent programs as state space automata

The notions we've seen of states , traces , and state spaces aren't specific to Promela, but are useful in any formalization of concurrent systems.In fact, we are ready to give one precise definition of a ``concurrent system'' in terms states and traces.It is similar to many conventional automata definitions , but includes a way to relate the current state to propositions , which we can later construct formulas out of.

State Space Automaton

A State Space Automaton $A$ is a tuple where:

• $S$ is a set of states. As before , a state is an assignment to all program variables (both local an global),including the program counter (line number) for each process.
• $s_0\in S$ is the initial state or start state .
• $T\subseteq S\times S$ is the transition relation . Equivalently, this is the edge relation of the state space .
• $\mathrm{Prop}$ , a set of propositions.
• $P:S2^{\mathrm{Prop}}$ is a mapping which, given a state, indicates all the properties that are true in that state.

It is the set $\mathrm{Prop}$ which will allow us to talk about our program variables in our logic formulas.The elements of $\mathrm{Prop}$ are simple propositions involving program variables. For example,

• $\mathrm{philosopher\_2\_has\_fork}$
• $\left(\mathrm{ctr}> 3\right)$
• $\mathrm{(in[].size()\; ==\; max\_buffer\_size)}$ (that is, the buffer in[] is full)