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.