FrequentlyAsked Questions about RTSpin

Q1. What is Spin, by the way ?
A1. Spin is a tool for ``system validation'', that is, convincing yourself
that your system does what it is supposed to do. Spin offers a language
(Promela) which allows you to describe your system, as well as its requirements,
in a formal way. Then, taking this specification as input, Spin generates
code (in C) for analysing your specification. Analysing might mean:

perform a random simulation

perform a partial correctness search

perform an exhaustive (total) correctness search
Correctness might mean:

absence of violated "assertions"

absence of deadlocks

absence of "bad" (acceptance) cycles

satisfaction of a general LTL formula
An assertion is a logical expression you can put in certain places in your
specification. It specifies an ``invariant'' of the system, i.e. "whenever
my system is in this state, this expression should be true". A deadlock
is a state where the system cannot advance any more. (For programs that
might stop, however, you can specify a set of ``valid endstates''). A
bad cycle is an infinite execution, where the system repeatedly does something
wrong, or never does anything good. You can specify things which shouldn't
be done repeatedly by labeling the corresponding states as "accept" (the
terminology comes from the automatatheoretic community), and things which
should be done repeatedly by labeling the corresponding states as "progress".
A LinearTemporalLogic (LTL) formula can express properties more complex
than "never happening" or (its negation) "repeatedly happening". For example,
you might want to say that "something happens continuously until something
else happens, if the later ever happens".

Q2. What does RealTime Spin add to Spin ?
A2. In Spin (or rather, its language Promela) the notion of time is
``qualitative''. This means that you can say things about the *order* of
events, such as "always, repeatedly, before" etc. But you cannot specify
``quantitative'' properties, like "event A happens at least 3 time units
before event B". RealTime Spin (or rather, the extended language RealTime
Promela) offers mechanisms to do this, by means of special continuous (realvalued)
variables, called ``clocks''. Clocks can be used to count the delay between
the execution of two or more statements in your program. You can constrain
such delays to be equal to, less than, or greater than a specific value,
or even to lie in an certain interval. Notice that clock count "real" time
(that is, dense time) so that strict bounds are also allowed. For instance,
you might want to say that an event happens strictly before 3 time units,
by using a clock x, and the constraint: x<3. Clocks can be reset, so
that they are reused. In RealTime Promela, clocks can only be reset to
zero, essentially for simplicity reasons. This model is equivalent to one
where clocks could be reset to any natural constant.

Q3. Why dense time ?
A3. See Alur's thesis: "Techniques for Automatic Verification of RealTime
Systems", Stanford Univ. 1991, chapter 1.

Q4. Why ``abstract'' time (i.e. time "units" instead of seconds, minutes,
hours, etc) ?
A4. Because programs and protocols, should generally be correct independently
of the underlying machine (or living being !) upon which they're executed.
That is, it is the *ratios* between time delays which should count, not
the exact delays. In any case, the abstract model is more general than
a concrete one: indeed, you can fix the time granularity of your specification
as you wish: you can take time units in your program to be seconds, or
lightyears ! Be careful, however, not to mix the two but only after performing
the necessary multiplications !

Q5. Can RealTime Spin verify the same properties as Spin ?
A5. There is no problem with the socalled ``safety'' properties. These
properties can be verified by simply looking at (finite) prefixes of infinite
executions. In other words, once such a property is falsified, there is
no future remedy. (This is not the case with ``liveness'' properties, for
which a finite prefix can always be extended to an infinite one, such that
the latter satisfies the property.) Practically, safety properties are
expressed as: "always P" (or, equivalently, "never (not P)") where P is
a proposition which can be evaluated by simply looking at the current state
of the system. (Correctly speaking, P can be in general any ``pasttime''
formula, i.e., that involves already seen states. The important thing is
that P cannot involve the system's future.) Safety properties cover most
of the interesting properties to be verified on a system. Assertions, deadlocks,
as well as many other general LTL properties fall into this category. All
of them present no problem to RealTime Spin. Liveness properties, on the
other hand, present a problem: verifying such properties in the untimed
context, comes down to finding acceptance cycles (i.e., cycles passing
from states labeled as "accept") in the reachability graph of the system.
These cycles represent in fact infinite executions of the system, where
a sequence of states and transitions is repeated over and over. In the
realtime context, there is the additional condition that these cycles
should be ``nonzeno''. Zeno cycles correspond to nonrealistic executions
where time is blocked, thus, such cycles should not be considered at all
during the analysis. (See Q7 for more on zeno cycles.)

Q5.1. Can RealTime Spin verify properties that Spin cannot ?
A5.1. It can, and this is no surprise, since RealTime Spin can deal
with quantitative time. Most useful are ``timebounded response properties'',
having the form: "if P occurs, then Q will follow in at most c time units".
You can use a "monitor process" as the one shown below, to verify that
your system satisfies such a property:
proctype MonitorBoundedResponse()
{
do
:: atomic{ reset(z) (P); break }
:: skip
od;
do
:: atomic{ when{z<=c} (Q); goto end_ok }
:: atomic{ when{z<=c} (!(Q)); skip }
:: atomic{ when{z>c} (!(Q)); goto error }
od;
error:
assert(0);
end_ok:
skip
}
This process verifies the "realtime" LTL formula: Always( P => Eventually_{in
<= c time units} Q ) (see Q6 on realtime LTL).
NOTICE on the implementation of Monitor: this process plays the role
of the Buchi automaton in classical Spin (the socalled ``never claim'').
This means that it must be synchronized with the system, so that each action
of the latter is followed (in zero time) by an action of Monitor. This
can be done by using a global boolean variable which schedules the system
and the monitor in a roundrobin manner, plus a global clock which constraints
the passage of time between the system and the monitor to zero. (This is
quite awkward, but for the moment it's the only solution I have. The problem
is that the never claim cannot be used in this case, since it executes
*before* the system, so it monitors in fact the *previous* system state.
This presents no problem in untimed semantics, since there is no exact
delay between transitions anyway, but in realtime it does make a difference.)
Q5.2. How can one tell a safety property from a liveness property ?
A5.2. There exists a mathematical characterization of safety and liveness
properties, in topological terms. However, this is not very useful in practice.
More useful are some rules of thumb, telling you that your property is
a safety one:
 if it is expressed as "always P" (or, equivalently, "never (not P)"),
where P is a general ``pasttime'' formula (see Q5 above).  if you are
searching simply for assertion violations, or deadlocks.  if you are using
a Buchi automaton arriving to a single acceptance state, which has a skiploop
to itself. (On the other hand, if you have to leave an acceptance state
and enter back then it's liveness.)
Q6. Is there a ``RealTime LTL'' ? Can it be used in RealTime Spin
?
A6. The realtime version of LTL is undecidable, once we permit strict
time constraints in its modalities, for example:
P => Eventually_{in = b time units} Q
However, it is decidable if we restrict ourselves to looser constraints
like:
P => Eventually_{in [a,b) time units} Q
etc. (See Alur's thesis for more details, cf. Q3.) In any case, there
is no automatic translation from realtime LTL formulas to realtime Buchi
automata offered in RealTime Spin (as is the case with LTL > Buchi automata,
in Spin). You have to code your property into a timed Buchi automaton by
hand !
Q7. What is a zenocycle ?
A7. In the untimed context, there is no constraint on the time delay
consumed at each state. Thus, we might as well assume that this delay is
constant, so that in an infinite execution time progresses without bound.
In other words, given a cycle in the reachability graph of an untimed specification,
we can safely assume that each repetition of the cycle takes some time,
such that the sum of delays of infinitely many repetitions is infinite
(i.e., diverges). In the realtime context, however, there are constraints
on the transitions making up a cycle, so that the delay to take a full
round of the cycle might be bounded. What is worse, this delay might depend
on previous rounds, and might be forced to become smaller after each round,
so that the final sum of all delays is finite. (Take, for example, the
case where a clock is never reset during the cycle, although it is upperbounded
at some point in the cycle.) This actually means that the cycle cannot
be executed an infinite number of times, since it does not let time progress
to infinity. (The underlying assumption here is that only finitely many
events can happen in a finite amount of time. This is reasonable for any
realistic system.) Such a cycle is called ``zeno'', by the name of Zeno,
the Greek philosopher of around 500 BC., disciple of Parmenides, founder
of Eleatic school. Zeno was the author of a number of paradoxes (such as
the paradox of Achilles and the tortoise) trying to disprove that plurality
and motion exist.

Q7.1 What does zenocycle detection mean ?
A7.1 Zeno cycles are not "real" cycles. They correspond to executions
where the system "overtakes time", since an infinite number of system actions
happen in a finite amount of time. Therefore, zeno cycles should be ignored
by the analysis, and the search should aim at nonzeno, acceptance cycles.
(One might wonder why not have a model which does not contain zeno cycles
at all in the first place. However, this is impossible to achieve: every
semantique model of realtime based on graphs (i.e., labeled transition
systems) is deemed to contain zeno cycles. It is much like the situation
with fairness: every graphbased semantic model of parallelism is deemed
to contain also unfair executions.) Zeno cycles are handled in RealTime
Spin by a zenocycle detection algorithm. Each time an acceptance cycle
is found, it is passed to this algorithm. If the latter decides that the
cycle is zeno, then the cycle is ignored and the search continues. If the
cycle is nonzeno, then it is announced as a (valid) acceptance cycle.
It should be noted that the invocation of the zenocycle detection algorithm
is optional: it is enabled by default, but can be disabled using the `z'
option of the analyser (tpan).

Q7.2 What's the use of zenocycle detection ?
A7.2 Zenocycle detection can permit the (semi) verification of liveness
properties (cf. Q5). Liveness properties can be verified by looking for
acceptance cycles in the reachability graph of the system. Usually, the
problem is coded in such a way, so that the correctness of the system is
equivalent to the *absence* of an acceptance cycle (automataemptyness
approach). In the realtime context, we are looking for acceptance cycles
which are also nonzeno. How can zenocycle detection help ? When performing
the search for acceptance cycles, each one found is tested for zenoness
(cf. Q7.1). At the end of the search, one of the following cases is possible:
 either no acceptance cycle is found whatsoever: in this case, the
property holds;  or, at least one nonzeno acceptance cycle is found:
in this case, the property does not hold, and the cycle can serve as a
counterexample.  or, all acceptance cycles found are zeno: in that case,
the analysis cannot conclude (this is what I call semidecidability).
Why is there a problem with the last case ? Since only zeno cycles have
been found, this means that no nonzeno cycle exists, right ? Unfortunately,
wrong. Indeed, there are examples containing both zeno and nonzeno acceptance
cycles, however, only zeno ones are found during the search, and the nonzeno
ones are missed. (This is due to the search algorithm of Spin, which does
not visit all possible cycles, i.e., all stronglyconnected components.)
In particular, the following program contains a nonzeno acceptance cycle
which is missed by the search:
clock x;
int a=0;
proctype P()
{
l0: when{x<=2} a=1;
l1: if
:: atomic{ when{x<=2} a=2; goto accept_l2 }
:: atomic{ when{x<=2} a=3; goto l3 }
:: atomic{ reset{x} a=4; goto l4 }
fi;
accept_l2: atomic{ when{x<=2} a=1; goto l1 };
l3: atomic{ when{x<=2} a=2; goto accept_l2 };
l4: atomic{ when{x<=2} a=3; goto l3 }
}
Try it out with rtspin, you'll get only two acceptance cycles: l1 > l2
> l1, and l1 > l3 > l2 > l1. The problem is that these are zeno cycles.
The nonzeno cycle is missed: l1 > l4 > l3 > l2 > l1.
Q8. Are transitions in RealTime Spin ``lazy'' or ``urgent'' ?
A8. Unlike other models, like Kronos' Timed Automata, there is no notion
of urgency in RealTime Spin. In particular, there is no way in RealTime
Spin to block time whatsoever: time passes while no transitions (i.e. statements)
are executed, and it can pass as long as it wishes. However, to be able
to fire a transition, the time guard of the latter must be satisfied. The
motivation for such a model is to avoid time deadlocks, which can arise
by arriving to states where time cannot progress any more. (Notice that
this is different from *cycles* where time does not progress. Indeed, a
cycle represents a *specific* (set of) execution(s) where it might be the
case that time blocks. Instead, if a state blocks time, then *no* future
execution starting from that state can let time progress.) On the other
hand, the model has its disadvantages, when one tries to express things
related to urgency. For instance, look at the example:
clock x, y;
int i;
proctype A()
{ when{ x==10 } i=i+1 }
proctype B()
{ when{ y==4 } i=i+1 }
Suppose that the initial values of i, x, and y are all 0. What are possible
final values for i ? Many would answer that there is just one such value,
namely, 2. However, this is not true in RealTime Spin. Indeed, the laziness
of the statement `when y==4 i=i+1' might prevent it from being executed
before time 4. After this time, the statement is no longer executable.
So, statement `when x==10 i=i+1' executes, and i gets the final value 1.
(Notice, however, that `when x==10 i=i+1' cannot be lazy, since it's the
only possible transition left.) The moral from this is: actions in RealTime
Spin are lazy, except from the latestintimepossible action, which is
executed at most in its latestintimepossible moments.
Back to home page of Stavros Tripakis