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 …
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 …
1. Matthew B. Dwyer ; George S. Avrunin ; James C. Corbett Patterns in Property Specifications for Finite-State Verification. pp. 411-420, ICSE 1999.

Home page

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License