Navigation
-
Content Actions
- Download module PDF
- Add to ...
- Rate this module (How does the rating system work?)
(0 ratings)
-
Recently Viewed
- This feature requires Javascript to be enabled.
Using Temporal Logic to Specify Properties
Note: Your browser may not currently support MathML. See our browser support page for additional details. You can always view the correct math in the PDF version.
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 of our particular tool weren't interested in, or hadn't thought of. Fortunately, SPIN does include a general property-checking mechanism: If we can state our property in a particular formal 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 how it uses temporal logic for verification.
First, we reflect that some properties — safety properties — can 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 properties — liveness properties — are about entire traces, not just some state in a trace. For instance, non-progress cycles is a cycle which does not contain any 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 logic — a temporal logic specifically designed to be conducive to expressing concepts which arise in concurrent programming. But before we can even do that, we need a clear model of concurrent 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.
- Definition 1: State Space Automaton
- A State Space Automaton
A S s 0 T Prop P -
S -
s 0 ∈ S -
T ⊆ S × S -
Prop -
P S 2 Prop
-
It is the set
-
philosopher_2_has_fork -
ctr > 3 -
(in[].size() == max_buffer_size) in[]is full)
- Definition 2: Trace
- Given a state space automaton, a trace
σ ω σ 0 σ 1 σ 2 T
Thus a trace is a path through the state space (as we have already seen). Now that we have logic propositions associated with each state, we can see that during a trace, those propositions will change their truth value over time. We'll illustrate this with diagrams like the following.
 |
In this example,
Although a bit unintuitive at first, it will be convenient to convert
all finite traces into infinite ones.
To do the conversion, we simply envision that once the automaton
reaches its ostensibly last (
- Definition 3: Stutter-Extend
- The finite trace
σ 0 σ n σ 0 σ n σ n σ n
To ensure this still satisfies the definition of a trace (where successive states must obey the automaton's transition relation), it is often assumed that every state has a transition to itself. Note that this convention precludes assuming that something must change between one state and the next, which is plausible since we are modeling asynchronous systems. This will be reflected in our formal logic below, which will have no built-in primitive for ``the-next-state''.
State Formulas
Now that we have a formal model of what a trace is,
we can start to make formal statements about what happens in a trace.
The simplest statements are state formulas,
i.e., propositional formulas
built out of
Notation Abuse Alert:
Deciding whether some particular state of a trace satisfies a formula also depends implicitly on the automatonExample 1
For example, given a trace
Example 2
Consider the trace
|
For which
However it doesn't make sense a priori to ask
whether an
entire trace satisfies some
particular state formula;
unlike regular propositional logic, the truth of state formulas
changes over time, as the trace
Introducing Temporal Connectives
So, how do we talk about formulas holding
(or not) over time?
In addition to making formulas out of
-
φ i φ i -
φ i φ i -
φ ψ i ψ φ -
ψ
As a mnemonic for the symbols ``
More formally, we define these connectives as follows.
- Definition 4: Always
σ i φ j i σ j φ Example
Figure 3: A generic trace σ σ i p p i 
Exercise 1
Decide whether each is true or false for following trace
|
-
σ 9 q -
σ 9 p -
σ 0 q -
σ 0 p q
Solution
-
True; from
σ 9 q -
True. Even stronger,
σ 7 p -
False, since
σ 3 q -
True, since at each individual index
i σ i p q
- Definition 5: Eventually
σ i φ k i σ k φ Example
Figure 5: A generic trace σ σ i q q k i 
Exercise 2
Decide whether each is true or false for the trace
-
σ 9 p -
σ 9 p -
σ 0 q -
σ 0 q -
σ 9 q p -
σ 0 p q
Solution
-
False; from
σ 9 p -
True.
This is a much weaker statement than
σ 9 p -
Extremely true, since
q σ 0 -
True, since
q σ 3 - False.
-
False. We already mentioned that
σ 0 p q σ 0 p q
Before continuing on with our two other connectives (strong- and weak-until), let's pull back a bit and look at our notation.
Notation Abuse Alert:
The nit-picky — er, the careful reader will have noticed that although we writedefinition:
Trace- Definition 6: Strong Until
σ i φ ψ k ≥ i σ k ψ j i j k σ j φ Example
Figure 6: A generic trace σ σ i r s r i k 1 
Exercise 3
Decide whether each is true or false for following trace
|
-
σ 0 q p -
σ 2 q p -
σ 5 q p -
σ 9 q p
Solution
-
True.
q σ 0 p σ 1 -
False.
Starting at
σ 2 p σ 5 q -
Very true, since
p σ 5 k j -
False. Since
p false σ 9 k ≥ 9 σ k p σ 9 q p
Exercise 4
Give the formal semantics of Weak Until (in the same way we
have given semantics for
Solution
Exercise 5
Weak Until could be omitted from our core set of LTL connectives,
since it can be defined in terms of the remaining connectives.
Provide such a definition.
That is, give an LTL formula
equivalent to
Solution
Here are three equivalent definitions. The first follows directly from the above exercise.
-
φ ψ φ φ ψ -
φ ψ φ φ ψ -
φ ψ φ ψ φ
Any logic that includes temporal connectives is a temporal logic. More specifically, this is Linear Temporal Logic (LTL). The ``linear'' part of this name means that we are looking only at individual traces, rather than making formulas that discuss all possible traces of a program. After all, a single program can result in many possible traces. An LTL formula does not allow us to say, for example, that a property holds in all possible executions of the program. However, SPIN overcomes some limitations by essentially testing an LTL formula against all possible traces. Will will return to SPIN in the next section.
In summary, the syntax used in SPIN is given by the following grammar.
| ltl | ::= | atom | ||
| | | (ltl binop ltl) | |||
| | | unop ltl | |||
| | | (ltl) | |||
| unop | ::= | [] | ``Always'' | |
| | | <> | ``Eventually'' | ||
| | | ! |
``Not'' | ||
| binop | ::= | U |
``Strong Until'' | |
| | | W |
``Weak Until'' | ||
| | | && |
``And'' | ||
| | | || |
``Or'' | ||
| atom | ::= | true |
||
| | | false |
|||
| | | #define'd identifiers |
Aside:
Some presentations of LTL use a box or ``G'' (Globally) for Always, and use a diamond or ``F'' for Eventually. Confusingly, some use ``U'' for Weak Until. Also, some include additional connectives like ``X'' (Next), which cannot be defined in terms of those given.Do we really need a whole new logic?
We could use regular ol' first-order logic
as our formal language for specifying temporal properties.
We'd do this by adding an explicit time index to
each proposition in
This approach, though, quickly becomes cumbersome.
Consider the everyday concept ``Someday, X will happen''.
We have to go through some contortions to shoehorn this concept into
first-order logic:
``There exists a day
The awkwardness stems from the fact that in English, ``eventually'', ``always'', and ``until'' are primitives. When we design a formal language to capture with these concepts, shouldn't we too include them as primitives? Having our formal representations reflect our natural conceptions of problems is the first law of programming!
This is why we have decided to incur the overhead of
defining a new language, LTL.
Still, you have noticed that the semantics we've given are phrased
in terms of ``
Translating between English and LTL: Examples
Let's look at how to turn a natural-English specification into temporal logic, and vice versa.
Example 3
How might we express the common client/server relationship
``if there is a request (
Hmm, that seems obvious:
Problem 1
Does the formula
Solution
That's only a bit better: it does now allow the implication
After more thought, we can get something which
does arguably match our intent:
However, even this may not be what everybody wants. Some considerations:
-
Even if
r s r s r s Figure 8: A trace showing multiple requests followed by a single servicing. 
-
A trace in which
s r φ -
Any trace in which requests are serviced
instantaneously will satisfy
φ Figure 9: A trace showing multiple requests and a single servicing. The servicing arguably corresponds to only the first request and might be an undesired behavior. 
- A trace in which a request is never made still satisfies this formula. While that is probably what is intended, it may not have occurred to you from the English statement alone.
Example 4
As a more complicated variation, we generally want to match
requests and their servicing. For example, what if there are two
requests,
Problem 1
As a partial solution, how can we express
``whenever
Solution
If we are also requiring that
Note that since LTL does not have quantifiers
(like
From these examples and the ones following, we can see that English is typically too ambiguous. To get the appropriate logic formula, we need to go back to the original problem and determine what was truly meant. Formalizing your specifications into temporal logic gives you the opportunity to closely examine what those specifications really should be.
Given a formula, try to understand it by translating it into English. Providing sample timelines that satisfy the formula is also quite helpful.
Exercise 6
Describe the meaning of
Solution
Literally, we can simply say
``always, eventually
More concise, though, is
``
 |
Exercise 7
Describe the meaning of
Solution
Again, a literal translation is ``always, if q then always not p''. Correct, but a bit more idiomatic-English would be ``whenever q, then forever not p'' or ``Once q, p is forever false''.
 |
Example 5
A railroad wants to make a new controller for single-track
railroad crossings.
Naturally, they don't want any accidents with cars at the crossing,
so they want to verify their controller.
Their propositions
Problem 1
Brainstorming:
Using natural English, what are some properties
we'd like to have true? Feel free to use words like
``always'', ``eventually'',
``while'', and ``until''.
You may add new propositions to
For each, feel free to demonstrate that the one property is not sufficient: give a trace which satisfies the property but is either unacceptable or unrealistic. (For instance, ``the gate is always down'' is safe but unacceptable; ``a train is always crossing'' is unrealistic since there aren't infinite trains.)
Solution
We can think of lots of examples, such as these.
- Whenever a train passing, the gate is down.
- If a train is approaching or passing, then the light is flashing.
- If the gate is up and the light is not flashing, then no train is passing or approaching.
- If a train is approaching, the gate will be down before the train passes.
- If a train has finished passing, then later the gate will be up.
- The gate will be up infinitely many times.
- If a train is approaching, then it will be passing, and later it will be done passing with no train approaching. (Thus, trains aren't infinitely long, and there are gaps between the trains.)
To formalize such statements, we would start with the primitive propositions involved. These could be
-
a -
p -
l -
g
This choice forces us to not refer to individual trains and, thus we must simplify some of our properties, e.g., ``If a train is approaching, the gate will be down before the next train passes.'' (Think about the consequences of not making this change.)
Some of these English descriptions are ambiguous, however. E.g., can a single train be approaching and passing simultaneously? When writing formal specifications, we'll be forced to think about what we mean to say, and provide an unambiguous answer, one way or the other. Continuing this example, we'll say that once a train is passing, it is no longer considered to be approaching.
Problem 2
Encode some of the properties from the previous exercise in temporal logic. It is often helpful to first turn the statement into a timeline (essentially a trace).
- ``Whenever a train passing, the gate is down.''
- ``If a train is approaching or passing, then the light is flashing.''
- ``If the gate is up and the light is not flashing, then no train is passing or approaching.''
- ``If a train is approaching, the gate will be down before the next train passes.''
- ``If a train has finished passing, then later the gate will be up.''
- ``The gate will be up infinitely many times.''
- ``If a train is approaching, then it will be passing, and later it will be done passing with no train approaching.''
Solution
Keep in mind that for any concept, there are many different (but equivalent) formulas for expressing it.
-
p g -
a p l -
g l p a -
Observe in the trace shown that in one instance, the gate goes down at the same time the train passes. In the LTL version we're using, we can't express the idea ``… strictly before the next train passes.'' Instead, we'll allow this simultaneity as a possibility.
Figure 12: A trace satisfying this property. 
a p g -
Figure 13: A trace satisfying this property. 
p p p g -
g -
Figure 14: A trace satisfying this property. 
a p p a
This last condition is not something that a controller
would enforce. Instead, we would expect the train
scheduling software to enforce this.
The controller would be allowed to assume this,
and we'd want to verify a property
Exercise 8
We've previously seen that SPIN knows some built-in concepts such as deadlock, livelock, weak- and strong-fairness. We'll see in the next section that SPIN can also be used to verify any LTL formula. But first, let's characterize some of those built-in concepts as LTL formulas using the context of a print server.
We will use the following propositions:
-
b assert(!).b -
e endlabel). -
p 1 p 2 progresslabel.2 -
r -
s
- No error occurs, i.e., we never reach a bad state.
- No deadlock occurs. (We'll take deadlock here to mean that all five of our variables stop changing; without having a different proposition for each state, this is close enough.)
- Progress is always made. That is, this trace doesn't go forever without making progress.
-
Weak Fairness:
if a request is made and held, it will get serviced.
I.e.,
it's not the case that a request stays
true - Strong Fairness: if a request is made infinitely often, then it will be serviced.
Solution
For each of these problems, there are many equivalent formulas, some of which are easier to verify as equivalent than others.
-
b -
b b p p r r s s e -
p 1 p 2 p 1 p 2 np_, which corresponds to ``all processes are in a non-progress state''. When SPIN does its built-in check for non-progress cycles, it actually just verifying!<>[]np_. You might recall that SPIN's idea of progress is state-based, not transition-based: SPIN (counterintuitively) considers it progress when a process does nothing but squat in aprogressstate. (This can only happen if weak fairness is not being enforced, or a guard is being labeled as progress.) How might we capture ``progress'' but still preclude those traces which just sit idly at a progress label? We could add a second progress label immediately followingp 1 q 1 q 2 p 1 q 1 p 1 q 1 -
``It's always not the case that
r s r s r r s -
r s
Exercise 9
For our simple producer/consumer model, what is the basic property we'd like to guarantee? Roughly, ``each product is consumed exactly once''. That is, Produce and Consume are called alternatingly, starting with Produce. (In particular, as stated this precludes modeling ``produce twice and queue the results''.)
Expressing this actually requires several clauses.
Give colloquial English translations of the following
LTL formulas.
We can make the generic model a bit concrete by
interpreting
-
finishProduce startConsume -
finishProduce startProduce finishConsume -
startConsume finishProduce -
finishConsume startConsume finishProduce
Solution
- If an ale is produced, then an ale will be consumed (possibly immediately). Note that we don't talk about which ale is consumed; in the following clauses we will try to enforce that it really is the same ale that was recently produced.
- If an ale is produced, then no ale-production is started until after an ale has been consumed.
- No ale is consumed before (an initial) ale is produced. Note that a trace in which no ale is ever produced still satisfies this formula.
- If an ale is consumed, nothing else will be consumed until an(other) ale has been produced.
Exercise 10
In the previous exercise, the formulas entailed that production of an item could not even begin until the previous object had been entirely consumed. This requirement might make sense for the interpretation of marathon training/running, but it doesn't seem essential to the production of hand-crafted ale, even if we do want to preserve the policy of never queuing up products.
Suppose we have a computer network port whose buffer can store only one web page's data at a time. The producer could correspond to some server sending a web page to that computer, and the consumer might be a browser which processes the data being received.
- Do we want to allow the producer to be producing the next product before the consumer finishes the current one?
- What change would you make to the formulas if you did want to allow this produce-while-consuming behavior (as in the ale interpretation)?
Solution
- No. That would mean the buffer is being overwritten with a new web-page's data, even though the browser is still trying to process the current page in the buffer.
-
We would replace
finishProduce startProduce finishConsume finishProduce finishProduce finishConsume
Note that we want to include the possibility that nothing is ever produced — we don't always want to enforce weak fairness. Consider an operating system's code for a print server — it is truly important that not owning a printer doesn't mean the OS always crashes!
Through this section, we've seen some of the common patterns that can arise in the formulas. Following upon the idea of Design Patterns as describing common programming idioms, ``Specification Patterns'' describe common logic specification idioms. For a list of LTL specification patterns, see Property Pattern Mappings for LTL.
In addition, there are also
algebraic equivalences for LTL,
just as there are for
propositional logic.
We have already seen a
DeMorgan-like
example; there are also less obvious equivalences, such as
distributing
Using Temporal Logic in SPIN
So, we have a Promela program and an LTL formula to verify. How do we use the tool? In SPIN, in the "Run" menu, select "LTL Property Manager". This opens a new window. The top half contains several subparts for entering an LTL formula, while the bottom half is for using it.
In the "Formula" textbox, you can type an LTL formula. If you prefer,
you can enter the operators using the buttons below,
rather than typing.
Also, you can use the "Load" button to restore a previously-saved LTL
formula from a file.
For a formula, the next checkboxes allow you to either verify that
the formula always holds or never holds.
The "Notes" textbox is simply descriptive text. If you plan on saving
the formula, it is helpful to remind yourself what this formula means
and is used for.
The "Symbol Definitions" textbox is where the LTL variables
(typically p,
q, etc.)
are related to the Promela code.
This is done through #defines
which are temporarily added to your Promela code.
Example 6
Let's consider another critical section example. The following code simply puts the critical section into a loop. Also included is our standard code to check that the mutual exclusion property is satisfied, although the assertion is commented out.
1 /* Number of copies of the process to run. */
2 #define NUM_PROCS 3
3
4 show bool locked = false;
5 show int num_crit = 0;
6
7 active[NUM_PROCS] proctype loop()
8 {
9 do
10 :: true ->
11
12 atomic {
13 !locked ->
14 locked = true;
15 }
16
17 /* Critical section of code. */
18 /* Something interesting would go here. */
19
20 num_crit++;
21 /* assert(num_crit == 1); */
22 num_crit--;
23
24 locked = false;
25 /* End critical section of code. */
26 od;
27 }
Using temporal logic, we can accomplish the same check without the assertion. There are several similar ways of doing this.
One way is to verify that num_crit
always has the value 0 or 1.
To do this, we'll make the following definition
in xspin's ``Symbol Definitions'' textbox:
#define p ((num_crit == 0) || (num_crit == 1))
[]p
and mark that we always want this formula to hold.
To verify with this formula is a two-step process. First, using the "Generate" button generates what is known as a never claim, shown in the window. This is more Promela code that is temporarily added to your program. This creates a special process that checks the LTL formula and is guaranteed to be executed after every normal step of your code. You don't need to understand the generated never claim, although SPIN presents it for advanced users. The never claim uses a couple syntactic features of Promela not covered in this module. Next, using the "Run Verification" button opens a small version of the verification options window that we're already familiar with. Running the verification puts any output in the LTL window.
Using spin from the command-line:
To verify temporal formulas from the command-line, you need to do three things: First, generate anever claim using
spin -f formula.
For example,
prompt> spin -f '[] (p -> <> (q || !r))'
never claim),
and paste it at the end of your Promela source file.
Also add #defines to the top of your file,
defining each propositional variable used in your LTL formula.
Finally, verify the resulting code.
Example 7
Generate and verify the code from the previous example.
The automatically-generated never claim is shown below.
It uses labels and
gotos which we haven't discussed,
but which will be familiar to many programmers.
(This code represents a small automaton, in this case with
two states, which gets incorporated into the larger
state space automaton that we've described.)
The use of the constant 1 here
is equivalent to the more mnemonic true.
never { /* !([]p) */
T0_init:
if
:: (! ((p))) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all
skip
}
Running the verification, it does not report any errors. However, note that verifying an LTL property automatically turns off deadlock checking:
Full statespace search for:
…
invalid end states - (disabled by never claim)
unreached in proctype loop
line 27, "pan.___", state 11, "-end-"
(1 of 11 states)
Exercise 11
We want to accomplish the same goal as the previous example, but with a formula that should never hold. What's an appropriate formula?
Solution
Using the same definition of p,
we can simply use <>!p.
I.e., we don't want it to ever happen
that p is false.
Exercise 12
Now let's verify something that can't be done easily with just
assertions. We also want to make sure that
num_crit
continually alternates between the values of 0 and 1, rather than
maintaining the same value. How can we do this?
Solution
Use the following symbol definitions:
#define p (num_crit == 0)
#define q (num_crit == 1)
([]<>p) && ([]<>q)
Exercise 13
How could we use LTL to verify whether no process is starved? Of course, this verification should fail, generating a trail where at least one process is in fact starved.
Solution
In essence, we want to verify
([]<>(_pid == 0)) && ([]<>(_pid == 1)) && ([]<>(_pid == 2))
_pid
is a local variable to each process,
but, unfortunately,
never claims are their own separate process,
and can't access those variables.
One solution is to create an equivalent global variable:
pid running;
Inside the critical section code add the line
running = _pid;
#define p (running == 0)
#define q (running == 1)
#define r (running == 2)
([]<>p) && ([]<>q) && ([]<>r)
Aside:
The never claim's process will numbered higher than any started by anactive proctype.
So, in this case, its PID is 3.
As expected, the verification fails, and a trail file is created. In the author's sample verification, this trail has only processes 0 and 1 entering the critical section, although there are many possible counter-examples.
It turns out, SPIN has a special syntax to express
whether a certain process is at a certain label.
So instead of defining a new variable,
we could alternately go to the critical section
and add a new label (say ``crit:'')
and then define:
#define p (loop[0]@crit) /* 0th 'loop' process is at crit. */
#define q (loop[1]@crit) /* 1st 'loop' process is at crit. */
#define r (loop[2]@crit) /* 2nd 'loop' process is at crit. */
Footnotes
-
Technically, these diagrams are a bit too suggestive:
a trace is only a sequence of discrete states,
with no concept of time existing in between states.
And the numbering of the
x true false P - Promela does includes a
handy syntax for testing whether a particular process
is at a particular label:
``
philosopher[3]@eating'' is true when the fourth (0-indexed)philosopherprocess is at the labeleating.
Comments, questions, feedback, criticisms?
Send feedback
- E-mail the authors of the module, Using Temporal Logic to Specify Properties
Footer
More about this content: Metadata | Version History
This work is licensed by Ian Barland, John Greiner, and Moshe Vardi under a Creative Commons Attribution License (CC-BY 1.0), and is an Open Educational Resource.
Last edited by John Greiner on Oct 6, 2005 3:43 pm GMT-5.