Time-constrained Universality
| Pattern Name and Classification | ||
| Time-constrained Universality: Real-time Occurrence Specification Pattern | ||
| Structured English Specification | ||
| description … | ||
| Pattern Intent | ||
| Thia pattern describe a portion of a system's execution which contains only states that have a desired property within a given timebound. | ||
| Temporal Logic Mappings | ||
| MTL | Globally: | $[\;]\;<c \; (P)$ |
| Before R: | $<>R \rightarrow ((P \cup R) \;|\; [\;]\;<c\;(P))$ | |
| 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 an extension of the pattern proposed in [1]. This pattern is closely related to the Time-constrained Absence and Time-constrained Existence patterns. Universality of a state can be viewed as absence of its negation. For event-based formalisms, we look for the existence of the positive event and absence of the negating event. | ||
| 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.