Promela |
Declarator |
progress |
NAME
progress -
label-name prefix for specifying liveness properties.
SYNTAX
progress[a-zA-Z0-9_]*: stmnt
DESCRIPTION
A progress label is any label name that starts with the
eight-character sequence
progress . It can appear anywhere a label can appear.
A label always prefixes a statement, and thereby uniquely identifies a local process state (i.e., the source state of the transition that corresponds to the labeled statement). A progress label marks a state that is required to be traversed in any infinite execution sequence.
A progress label can appear in a proctype , or trace declaration, but has no special semantics when used in a never claim or in notrace declarations. Because a global system state is a composite of local component states (e.g., proctype instantiations, and an optional trace component), a progress label indirectly also marks global system states where one or more of the component systems is labeled with a progress label.
Progress labels are used to define correctness claims. A progress label states the requirement that the labeled global state must be visited infinitely often in any infinite system execution. Any violation of this requirement can be reported by the verifier as a non-progress cycle.
EXAMPLES
active proctype dijkstra() { do :: sema!p -> progress: sema?v od }The requirement expressed here is that any infinite system execution contains infinitely many executions of the statement sema?v .
NOTES
Progress labels are typically used to mark a state where effective
progress is being made in an execution, such as
a sequence number being incremented or valid data being accepted
by a receiver in a data transfer protocol.
They can, however, also be used during verifications
to eliminate harmless variations of liveness violations.
One such application, for instance, can be to mark message loss
events with a pseudo
progress label, to indicate that sequences that contain infinitely many
message loss events are of secondary interest.
If we now search for non-progress executions, we will no
longer see any executions that involve infinitely many
message loss events.
Spin has a special mode to prove absence of non-progress cycles. It does so with the predefined LTL formula:
(<>[] np_)which formalizes non-progress as a standard Buchi acceptance property.
The standard stutter-extension, to extend finite execution sequences into infinite ones by stuttering (repeating) the final state of the sequence, is applied in the detection of all standard types of acceptance properties, but it is not used for non-progress cycles.
The manual page for never claims describes how the predefined variable np_ can also be used to restrict a verification to precisely the set of either progress or non-progress cycles.
SEE ALSO
accept
end
labels
ltl
never
np_
trace
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 19 August 2008) |