Given a model system specified in Promela, Spin can perform random or interactive simulations of the system's execution or it can generate a C program that performs a fast exhaustive verification of the system state space. During simulations and verifications Spin checks for the absence of deadlocks, unspecified receptions, and unexecutable code. The verifier can also be used to prove the correctness of system invariants and it can find non-progress execution cycles. Finally, it supports the verification of linear time temporal constraints; either with Promela never-claims or by directly formulating the constraints in temporal logic.
The verifier is setup to be fast and to use a minimal amount of memory. The exhaustive verifications performed by Spin are conclusive. They establish with certainty whether or not a system's behavior is error-free. Very large verification runs, that can ordinarily not be performed with automated techniques, can be done in Spin with a ``bit state space'' technique. With this method the state space is collapsed to a few bits per system state stored. Although this technique doesn't guarantee certainty, the coverage is better, and often much better, than that obtained with traditional random simulation.
The syntax of Promela is C-like. Below, our tendency is to use examples for those parts that are similar to C, but we attempt to be more precise elsewhere.
active assert atomic bit bool break byte chan d_step D_proctype do else empty enabled fi full goto hidden if init int len mtype nempty never nfull od of pc_value printf priority proctype provided run short skip timeout typedef unless unsigned xr xs
#define NAME 5The second method is to use the keyword mtype; see symconst.
+ - * / % > >= < <= == != ! & || && | ~ >> << ^ ++ -- len() empty() nempty() nfull() full() run eval() enabled() pc_value()Most operators are binary. The logical negation (!) and the minus (-) operator can be both unary and binary, depending on context. The ++ and -- operators are unary suffix operators, like they are defined in C. The exclusive-or is ^. The functions on the one-but-last line are unary and apply only to message channels (see MsgChan); len measures the number of messages an existing channel holds; the other channel operators have the expected meaning and are introduced to assist partial order reductions; see pored. These functions cannot be used in larger expressions. E.g., !empty(q) will result in a syntax error and nempty(q) should be used instead. The unary functions on the last line are special. The first operator is used for process instantiation (see Processes below). When executed it yields the instantiation number of the instance it created. The second one is discussed in ChanOps and the others in never. The operators on the first four lines are defined as in C. Promela follows the C-convention that the boolean false-condition corresponds with the value 0; any non-zero value denotes truth.
(expr1 -> expr2 : expr3)has the value of expr3 if expr1 evaluates to zero, and the value of expr2 otherwise. Note that -> is required here and cannot be replaced by a ;.
byte name1, name2 = 4, name3An initializer, if specified, must be a constant. By default variables are initialized to zero. The bit-widths of these basic types are, respectively, 1, 1, 8, 16 and 32. The last two are signed quantities; the first three are unsigned. A variable can have a user-defined type as well; see structs.
int name[4]An array can have a single constant as an initializer, initializing all array elements. Array indices start at 0, as in C; hence, the largest index would be 3 in this case.
mtype = {OK, READY, ACK}
and variables of this type by
mtype Status = OK;Only one mtype-definition is allowed which must be global and at most 256 symbolic constants can be declared; an mtype variable is 8 bits wide.
The advantage of mtypes over #defines is that the former type of symbolic constants is recognized by Spin and during simulations the symbolic names are used instead of the values they represent.
chan Transfer = [2] of {mtype, bit, short, chan};
chan Device[3] = [0] of {byte};
chan Channel;
Here, Transfer can store up to 2 messages in the channel; the message
type is indicated between the braces (in this case each message consists of
4 parts). Device is an array of channels; each channel is
synchronous, i.e., sends and receives must synchronize as no messages can
be stored. Finally, Channel is an uninitialized channel that can be
used only after an initialized channel has been assigned to it.
Note that an object of type chan can be part of a message declaration in another channel.
xr Transfer; xs Channel;in some process, declares that this process is the only one to receive messages on Transfer and the only one to send on Channel.
It is a run-time error if during analysis it turns out that some other process receives from Transfer or sends to Channel.
See Reductions for more detail.
typedef Msg {
byte a[3], b;
chan p
}
that can be used in variable declarations and, more generally, wherever
a type definition is needed:
Msg foo;
chan stream =[0] of {mtype,Msg}
Elements of structures are accessed as in C; e.g.,
foo.a[1]
hidden int fooA hidden variable is not part of the system state (see Execution) and its value is always undefined, although it can be assigned to. It is useful when a `scratch' variable is needed, e.g., to flush the values in a channel buffer, because it does not add to the size of the state-vector during analysis and thus reduces the memory requirements for analysis; cf. MemTim.
Only global declarations can be thus qualified; elements of a structure are considered local. Bit, bool and channel variables cannot be hidden.
There is a pre-declared hidden variable, _, which can be assigned to in any context. Its (implicit) type is int so that it can be used to assign bit, bool, byte, mtype, short and int values to.
proctype pname( chan In, Out; byte id )
{ statements }
Such a process is instantiated by a run-operation:
run pname(Transfer, Device[0], 0)that first assigns the actual parameters to the formal ones and then executes the statements in the body. Each process instance has a unique, positive instantiation number, which is yielded by the run-operator (and by pid); see specvar. A process-instance remains active until the process' body terminates (if ever).
Processes cannot have arrays as (part of) a formal parameter type, but structures are allowed.
Process declarations can be augmented in various ways. The most general form is
active [N] proctype pname(...) provided (E) priority MThe active modifier causes N instances of the proctype to be active in the initial system state, where N is a constant. If [N] is absent, only one instance is activated. Formal parameters of instances activated through the active modifier are initialized to 0; i.e. actual parameters can only be passed using run-statements.
A proctype can have an enabling condition E associated with it, which is a general side-effect free expression that may contain constants, global variables, the predefined variables timeout and pid, but not other local variables or parameters, and no remote references. Enabling conditions are evaluated once, in the initial state.
For use during random simulations, a process instance can run with a priority M, a constant >=1. Such a process is M times as likely to be scheduled than a default (priority 1) process. Execution priorities can be used in a run-statement as well:
run pname(...) priority MA process instantiated with a run statement always gets the priority that is explicitly or implicitly specified there (the default is 1).
Note that priorities have no effect during analysis.
D_proctype pname( chan In, Out; byte id )
{ statements }
declares that any instance of pname is deterministic.
It has no other effect, then causing an error during analysis if some
instance is not.
Note that determinism is a dynamic property. E.g., if pname has in its body the statement
if :: In?v -> ... :: Out!e -> ... fithen non-determinism is flagged only if during some computation, there is an instance of pname for which the receive and send on the actual channels bound to In and Out are simultaneously enabled.
init { statements }
This process, if present, is instantiated once, and is often
used to prepare the true initial state of a system by initializing
variables and running the appropriate process-instances.
never { statements }
is a special type of process that, if present, is instantiated once.
As explained further in tempclaim, never claims are used to
detect behaviors that are considered undesirable or illegal.
The individual statements in statements are interpreted as conditions (see Exec and ExprStat) and, therefore, should not have side-effects (although this will cause warnings rather than syntax-errors).
Statements that can have side-effect are assignments, auto-increment and decrement operations, communications, run and assert statements.
Never claims can use three additional functions:
_pid, _last_pid is a predefined local variable that holds the instantiation number of the process' instance. _last is a predefined global variable that holds the instantiation number of the process instance that performed the last step in the current execution sequence. Initially, _last is zero.
procname[pid]@labelis true precisely if the process with instantiation number pid of proctype procname is currently at the statement labeled with label.
assert assignment atomic break declaration d_step else expression goto receive selection skip repetition send timeout unlessIn particular, note that expressions can be used as statements as well.
Statements are separated by either a semi-colon (;) or, equivalently, an arrow (->). The arrow is sometimes used to indicate a causal relation between successive statements and also in selection and repetition statements to separate the guard from the statements it is guarding; see select and repet.
Statements that have no smaller statements as a constituent, are called basic. E.g., an assignment is a basic statement whereas a selection is not.
assert( expression )aborts the program if the expression returns a zero result; otherwise it is just passed.
atomic { statements }
attempts to execute the statements in one indivisible step;
i.e., without interleaved execution of other processes.
An atomic statement is enabled if its first statement is.
Making local computations atomic can effect important reductions of the complexity of the verification system; cf. MemAtD.
During its execution, control can only be transferred outside the scope of an atomic statement by an explicit goto or at a point where a statement within its scope becomes blocked. If this statement subsequently becomes enabled again, execution may continue at that point.
There is no constraint on what may occur inside the scope. In particular, it is possible to jump to any (labeled) location within the scope of an atomic.
The body of a process instance activated by a run-statement is considered to be outside the scope of the atomic statement performing the activation.
goto labeltransfers control to the statement labeled by label which has to occur in the same procedure as the goto.
d_step { statements }
has the same effect as atomic but is even more efficient;
cf. MemAtD.
However, statements within its scope must be completely
deterministic; they may not jump to labels outside the d_step's
scope; there may be no jumps from the outside to labeled statements
within the scope; remote references (see RmtRef) are disallowed.
Finally, statements other than the first may not block. A d_step
is enabled precisely if its first statement is.
Promela considers the location in front of the d_step to be
within its scope and the location just after its last statement to be
outside. Hence, to achieve the intended effect of the following
incorrect code-fragment:
goto label;
...
label:
d_step {
...
do
...
break
...
od
}
use this code instead:
goto label;
...
label: skip;
d_step {
...
do
...
break
...
od; skip
}
For example, instead of writing a busy wait loop
while (a != b) skipthe same effect is achieved in Promela by the statement
(a == b)
q!var1,const,var2,... or, equivalently q!var1(const,var2,...) q?var1,const,var2,... or, equivalently q?var1(const,var2,...)Are the standard channel operations; the first is a send statement, the second a receive. Here, q denotes a channel and the list var1,const,var2,... should be compatible with the channel's message type. For a send or receive to be enabled, q has to be initialized. Furthermore, if the channel is buffered, a send is enabled if the buffer is not full; a receive is enabled if the buffer is non-empty. On an unbuffered channel, a send (receive) is enabled only if there is a corresponding receive (send) that can be executed simultaneously. A receive statement executes by reading the oldest message on the channel; if the channel is unbuffered, it reads the message of the simultaneously executing send statement. A send statement executes by putting its message in the buffer (if there is one). Note that a channel operation on an unbuffered channel can only execute if a matching operation executes simultaneously.
Constants in the list of a receive, constrain its enabledness by forcing the corresponding values in the oldest message (or matching send) to be the same; if not, the receive is blocked.
It is possible to use a local or global variable to likewise constrain a channel operation's enabledness:
q?var1,eval(var2),var3blocks in case a matching send's 2nd value does not equal the value of var2. Note that the value of var2 is not changed.
For buffered channels, there are additional operations:
if :: statements ... :: statements fiSelects one among its options (each of them starts with ::) and executes it. An option can be selected if its first statement (the guard) is enabled. A selection blocks until there is at least one selectable branch. If more than one option is selectable, one will be selected at random. The special guard else can be used (once) in selection and repetition statements and is enabled precisely if all other guards are blocked. It may not be used if a send or receive statement is used as guard.
do :: statements ... :: statements odSimilar to a selection, except that the statement is executed repeatedly, until control is explicitly transferred to outside the statement by a goto or break. A break will terminate the innermost repetition statement in which it is executed and cannot be used outside a repetition.
{ statements-1 } unless { statements-2 }
Starts execution in statements-1.
Before each statement in statements-1 (including the first one)
is executed, enabledness of statements-2 is checked and if it
is, execution of statements-1 is aborted and control transfers
to statements-2; control remains in statements-1,
otherwise.
If statements-1 terminates, statements-2 is ignored.
In an unless, a d_step, in contrast with an atomi