Existence Property Pattern
Untimed existence
The Existence Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on Untimed version.
Time-constrained version
| Pattern Name and Classification | ||
| Time-constrained Existence: Real-time Occurrence Specification Pattern | ||
| Structured English Specification | ||
| description … | ||
| Pattern Intent | ||
| This pattern aims at describing a portion of a system's execution bounded by a time interval that contains an instance of certain events or states. | ||
| Temporal Logic Mappings | ||
| MTL | Globally: | $<> \;<c \;(P)$ |
| Before R: | $!R \; W \; (P \& !R)$ | |
| After Q: | $[\;](!Q) \; | <>(Q & <><c \;P))$ | |
| Between Q and R: | $[\;](Q \& !R -> (!R \; W (P \& !R)))$ | |
| After Q until R: | $[\;](Q \& !R -> (!R \cup (P \& !R)))$ | |
| TCTL | Globally: | $AF \; <c\;(P)$ |
| Before R: | $A[!R \; W \; (P \& !R)]$ | |
| After Q: | $A[!Q \; W \; (Q \& AF\;<c\;(P))]$ | |
| Between Q and R: | $AG(Q \& !R -> A[!R \; W \; (P \& !R)])$ | |
| After Q until R: | $AG(Q \& !R -> A[!R \cup (P \& !R)])$ | |
| Example and Known Uses | ||
| description … | ||
| Relationships | ||
| This pattern is the extension of the Existence pattern introduced by Dwyer in [1]. This pattern can be considered the dual of the Time-constrained Absence pattern. | ||
| Additional notes | ||
| description … | ||
Probabilistic version
The Existence Property Pattern has been proposed by Dwyer in [2] and it can be found on Probabilistic version.
Bibliography
1. Matthew B. Dwyer ; George S. Avrunin ; James C. Corbett Patterns in Property Specifications for Finite-State Verification. pp. 411-420, ICSE 1999.
2. Lars Grunske Specification patterns for probabilistic quality properties. ICSE 2008: 31-40