Time-constrained Absence
| Pattern Name and Classification | ||
| Time-constrained Absence: Real-time Occurrence Specification Pattern | ||
| Structured English Specification | ||
| description … | ||
| Pattern Intent | ||
| This pattern describes a portion of a system's execution that is free of certain events or states within a time-constraint. | ||
| Temporal Logic Mappings | ||
| MTL | Globally: | $[\;]\;<c\;(!P)$ |
| Before R: | $<>R \rightarrow (!P \cup R)$ | |
| After Q: | $[\;](Q \rightarrow [\;] \; <c\;(!P))$ | |
| Between Q and R: | $[\;]((Q \; \& \; !R \; \& <>R) \rightarrow (!P \cup R))$ | |
| After Q until R: | $[\;](Q \; \& \; !R \rightarrow (!P \;W \;R))$ | |
| TCTL | Globally: | $AG\;<c\;(P)$ |
| Before R: | $A[(!P \;| \;AG(!R)) \;W \;R]$ | |
| After Q: | $AG(Q \rightarrow AG\;<c\;(P))$ | |
| Between Q and R: | $AG(Q \& !R \rightarrow A[(P \;| \;AG(!R)) \;W \;R])$ | |
| After Q until R: | $AG(Q\; \& \;!R \rightarrow A[P \;W \;R])$ | |
| Example and Known Uses | ||
| description … | ||
| Relationships | ||
| This pattern is the extension of the Absence pattern introduced by Dwyer in [1]. This pattern can be considered the dual of the Time-constrained Existence pattern. | ||
| Additional notes | ||
| description … | ||
Bibliography
1. Matthew B. Dwyer ; George S. Avrunin ; James C. Corbett Patterns in Property Specifications for Finite-State Verification. pp. 411-420, ICSE 1999.