• 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 "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 end-states''). 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 automata-theoretic community), and things which should be done repeatedly by labeling the corresponding states as "progress". A Linear-Temporal-Logic (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 Real-Time 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". Real-Time Spin (or rather, the extended language Real-Time Promela) offers mechanisms to do this, by means of special continuous (real-valued) 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 Real-Time 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 Real-Time 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 light-years ! Be careful, however, not to mix the two but only after performing the necessary multiplications !

• Q5. Can Real-Time Spin verify the same properties as Spin ?

• A5. There is no problem with the so-called ``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 ``past-time'' 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 Real-Time 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 real-time context, there is the additional condition that these cycles should be ``non-zeno''. Zeno cycles correspond to non-realistic 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 Real-Time Spin verify properties that Spin cannot ?

• A5.1. It can, and this is no surprise, since Real-Time Spin can deal with quantitative time. Most useful are ``time-bounded 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 "real-time" LTL formula: Always( P => Eventuallyin <= c time units Q ) (see Q6 on real-time LTL).

NOTICE on the implementation of Monitor: this process plays the role of the Buchi automaton in classical Spin (the so-called ``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 round-robin 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 real-time 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 ``past-time'' 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 skip-loop 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 ``Real-Time LTL'' ? Can it be used in Real-Time Spin ?

• A6. The real-time version of LTL is undecidable, once we permit strict time constraints in its modalities, for example:

P => Eventuallyin = b time units Q

However, it is decidable if we restrict ourselves to looser constraints like:

P => Eventuallyin [a,b) time units Q

etc. (See Alur's thesis for more details, cf. Q3.) In any case, there is no automatic translation from real-time LTL formulas to real-time Buchi automata offered in Real-Time 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 zeno-cycle ?

• 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 real-time 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 upper-bounded 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 zeno-cycle 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 non-zeno, 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 real-time based on graphs (i.e., labeled transition systems) is deemed to contain zeno cycles. It is much like the situation with fairness: every graph-based semantic model of parallelism is deemed to contain also unfair executions.) Zeno cycles are handled in Real-Time Spin by a zeno-cycle 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 non-zeno, then it is announced as a (valid) acceptance cycle. It should be noted that the invocation of the zeno-cycle 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 zeno-cycle detection ?

• A7.2 Zeno-cycle 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 (automata-emptyness approach). In the real-time context, we are looking for acceptance cycles which are also non-zeno. How can zeno-cycle 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 non-zeno acceptance cycle is found: in this case, the property does not hold, and the cycle can serve as a counter-example. - or, all acceptance cycles found are zeno: in that case, the analysis cannot conclude (this is what I call semi-decidability).
Why is there a problem with the last case ? Since only zeno cycles have been found, this means that no non-zeno cycle exists, right ? Unfortunately, wrong. Indeed, there are examples containing both zeno and non-zeno acceptance cycles, however, only zeno ones are found during the search, and the non-zeno ones are missed. (This is due to the search algorithm of Spin, which does not visit all possible cycles, i.e., all strongly-connected components.) In particular, the following program contains a non-zeno 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 non-zeno cycle is missed: l1 -> l4 -> l3 -> l2 -> l1.
• Q8. Are transitions in Real-Time Spin ``lazy'' or ``urgent'' ?

• A8. Unlike other models, like Kronos' Timed Automata, there is no notion of urgency in Real-Time Spin. In particular, there is no way in Real-Time 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 Real-Time 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 Real-Time Spin are lazy, except from the latest-in-time-possible action, which is executed at most in its latest-in-time-possible moments.