Promela Reference -- trace(2)

Promela

Declarator

trace


NAME
trace , notrace - for defining event sequences as properties.

SYNTAX
trace { sequence }
notrace { sequence }

DESCRIPTION
Much like a never claim declaration, a trace or notrace 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 or notrace declaration must be globally declared message channels, and all message fields must either be globally known (possibly symbolic) constants, or the predefined global variable _ , which can be used in this context to specify don't care conditions. The structure and place of a trace event declaration within a Promela model is similar to that of a never claim: it must be declared globally.

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

An event trace declaration must always be deterministic.

A trace declaration specifies behavior that must be matched by the remainder of the specification, and a notrace declares behavior that may not be matched.

A notrace definition is subject to the same requirements as a trace definition, but acts as its logical negation. A notrace definition is violated if the event sequence that is specified can be matched completely, that is, if either a user-defined end state in the trace definition is reached, or the closing curly brace of the declaration.

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 of type a , and all receive operations on channel q2 are exclusively messages of type b , is written as follows:

NOTES
There are two significant differences between an event trace and a never claim declaration: First, an event trace matches event occurrences that can occur in the transitions between system states, whereas a never claim matches boolean propositions on system states.

A system state, for the purposes of verification, is a stable value assignment to all variables, process states, and message channels. 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 order that is given in the trace declaration.

The second difference is that 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.

An event trace automaton, just like a never claim automaton, has a current state, but it only executes transitions if one of the monitored events occurs. That is, unlike a never claim, it does not execute synchronously with the system.

It is relatively easy to monitor receive events on rendezvous channels with an event trace assertion, but very hard to do so with a never claim. Monitoring the send event on a rendezvous channel is also possible, but it would also have to match all rendezvous send offers that are made, including those that do not lead to an accepting receive event.

SEE ALSO
_
accept
assert
end
ltl
never
progress


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)