Promela Reference -- trace(2)

`trace(2)`

NAME
trace - for defining valid event sequences.

SYNTAX
trace { sequence }

DESCRIPTION
As with never claim declarations, a trace declaration does not specify new behavior, but instead states a correctness requirement on existing behavior in the remainder of the system. All channel names referenced in a trace declaration must be to globally declared message channels, and all message fields must be globally known (possibly symbolic) constants, or the predefined global variable _ . A trace declaration can be one of the modules of a Promela specification, i.e., it's structure and place within a Promela model is similar to that of an init , or never claim declaration.

An event trace declaration defines a correctness claim with the following properties.

Each channel name that is used in an event trace declaration is monitored for compliance with the structure and context of the trace declaration.
If only send operations on a channel appear in the trace, then only send operations on that channel are subject to the check. Similarly for receive operations. If both types appear, both are subject to the check, and they must occur in the relative order that the trace declaration gives.
An event trace declaration may contain only send and receive operations (i.e., events), but it can contain any control flow construct. This means that no global or local variables can be declared or referred to. This excludes the use of assignments and conditions. Send and receive operations are restricted to simple sends or receives; they cannot be variations such as random receive, sorted send, receive test, etc.
Message fields that must be matched in sends or receives must be specified either with the help of symbolic mtype names, or with constants. Message fields that have don't care values can be matched with the predefined write-only variable _ (see _(5)).
Sends and receives that appear in an event trace are called monitored events . These events do not generate new behavior, but they are required to match send or receive events on the same channels in the model, with matching message parameters. A send or receive event occurs whenever a send or a receive statement is executed, i.e., an event occurs during a state transition.
An event trace can capture the occurrence of receive events on rendezvous channels.
An event trace causes a correctness violation if a send or receive action is executed in the system that is within the scope of the event trace, but that cannot be matched by a monitored event within that declaration.
One can use accept , progress , and end -state labels in event trace declarations, with the usual interpretation.

Event traces must be deterministic (we may relax this restriction in furture releases.)

EXAMPLES
An event trace declaration that specifies the correctness requirement that send operations on channel q1 alternate with receive operations on channel q2 , and furthermore that all send operations on q1 are (claimed to be) exclusively messages with value a , and all receive operations on channel q2 are exclusively messages with value b , is written as follows:


trace {
        do
        :: q1!a; q2?b
        od
}

NOTES There are two significant differences between an event trace and a never-claim declaration: An event trace matches event occurrences that can occur in the transitions between system states, whereas a never claim matches propositional values on system states that exist between state transitions. A system state, for the purposes of verification, is a stable value assignment to variables, process-states, and message channels, that can be tested in boolean propositions. The transitions of a never claim are labeled with boolean propositions (expressions) that must evaluate to true in system states. The transitions of an event trace are labeled directly with monitored events that must occur in system transitions in the partial order that is stipulated in the trace declaration. An event trace monitors only a subset of the events in a system: only those of the types that are mentioned in the trace (i.e., the monitored events). A never claim, on the other hand, looks at all global systems states that are reached, and must be able to match the state assignments in the system at every state that is reached. An event trace automaton, just like a never claim automaton, has a current state, but it only executes transitions if a monitored event occurs in the system. (I.e., it does not execute synchronously with the system, as a never claim is required to do.) Note that it is easy to monitor receive events on rendezvous channels with an event trace , but very hard to do so with a never claim. Monitoring the send event on a rendezvous channel is also possible, but it would have to match also all rendezvous send offers, including those that cannot lead to an accepting receive event. SEE ALSO ltl(1), accept(2), end(2), notrace(2), never(2), progress(2), _(5). Spin Online References Promela Manual Index Promela Grammar Spin HomePage (Page Updated: 16 December 1997)

`Promela`

`Declarator`

`trace(2)`