Absence Property Pattern
Absence Property Pattern
Intent
To describe a portion of a system's execution that is free of
certain events or states. Also known as Never.
Mappings
Examples and Known Uses
The most common example is mutual exclusion. In a state-based
model, the scope would be global and P would be a state formula
that is true if more than one process is in its critical section.
For an event-based model, the scope would be a segment of the
execution in which some process is in its critical section (i.e.,
between an enter section event and a leave section event), and P
would be the event that some other process enters its critical
section.
Relationships
This pattern is the dual of the Existence pattern. In fact, in
many specification formalisms negation and explicit queries for
existence will be used to formulate an instance of the Absence
pattern, as seen in the examples above.
Note that Between scopes in this pattern (with a false proposition
or empty event symbol) appear to be able to specify the same thing
as a Response pattern with
global scope. This is not the case, however, since the cause-effect
relationship is required for the
Response whereas the scope for this pattern is optional.
If one wishes to exclude states characterized by multiple propositions
or multiple events one can do this by defining P appropriately.
One common use is to fill the role of P in the above mappings
with disjunctions of propositions or event symbols. For other
parameterizations of patterns
consult the pattern notes.
This is an Occurrence pattern.