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 …
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 …

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