Absence Property Pattern

Untimed version

This pattern has been proposed in [1].

Pattern Name and Classification
Absence: Occurrence Specification Pattern
Structured English Specification
Scope, it is never the case that P [holds]. (see the English grammar).
Pattern Intent
This pattern describes a portion of a system's execution that is free of certain events or states.
Temporal Logic Mappings
LTL Globally: $\Box (\neg P)$
Before R: $\Diamond R \rightarrow (\neg P \; \mathcal{U} \; R)$
After Q: $\Box (Q \rightarrow \Box (\neg P))$
Between Q and R: $\Box ((Q \wedge \neg R \wedge \Diamond R) \rightarrow (\neg P \; \mathcal{U} \; R))$
After Q until R: $\Box (Q \wedge \neg R \rightarrow (\neg P \; \mathcal{W} \; R))$
CTL Globally: $AG(\neg P)$
Before R: $A[(\neg P \vee AG(\neg R)) \; \mathcal{W} \; R]$
After Q: $AG(Q \rightarrow AG(\neg P))$
Between Q and R: $AG(Q \wedge \neg R \rightarrow A[(\neg P \vee AG(\neg R)) \; \mathcal{W} \; R])$
After Q until R: $AG(Q \wedge \neg R \rightarrow A[\neg P \; \mathcal{W} \; R])$
Additional notes
The Absence Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on Untimed version.

Time-constrained version:

Pattern Name and Classification
Time-constrained Absence: Real-time Occurrence Specification Pattern
Structured English Specification
Scope, it is never the case that P [holds] [ Time(0)]. (see the English grammar).
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: $\Box^{[t1,t2]}\;(\neg P)$
Before R: $\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P)))$
After Q: $\Box (Q \rightarrow \Box^{[t1,t2]}\;(\neg P))$
Between Q and R: $\Box((Q \; \wedge \; \Box^{[0,t1]} (\neg R) \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P)))$
After Q until R: $\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow (\neg P \;\mathcal{W}^{[t1,t2]} \;R))$
TCTL Globally: $AG\;^{[t1,t2]}\;(\neg P)$
Before R: $A(((\neg P \;\vee \;AG( \neg R)) \; \mathcal{U}^{[t1,t2]} \;R) \vee (G^{[t1,t2]}(\neg P \wedge \neg R) \; \mathcal{U}^{[t2,\infty)} \;R ))$
After Q: $AG(Q \rightarrow AG\;^{[t1,t2]}\;( \neg P))$
Between Q and R: $AG((Q \; \wedge \; AG^{[0,t1]} (\neg R)) \rightarrow A(((\neg P \;\vee \;AG( \neg R)) \;\mathcal{U}^{[t1,t2]} \;R) \vee (G^{[t1,t2]}(\neg P \wedge \neg R) \;\mathcal{U}^{[t2,\infty)} \;R )))$
After Q until R: $AG((Q\; \wedge \;AG^{[0,t1]} (\neg R)) \rightarrow A(\neg P \; \mathcal{W}^{[t1,t2]} \;R))$
Example and Known Uses
For security reasons, after a login failure the system must be free of login attempts between 10 to 50 milliseconds. In this example "after a login failure" represents the scope After Q.
Additional notes
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 Universality pattern.

Probabilistic version:

Pattern Name and Classification
Probabilistic Absence: Probabilistic Occurrence Specification Pattern
Structured English Specification
Scope, it is never the case that P [holds] [ Time(0)] [Probability]. (see the English grammar).
Pattern Intent
This pattern describes a portion of a system's execution that is free of certain events or states with a defined probability.
Temporal Logic Mappings
PLTL Globally: $[\Box^{[t1,t2]}\;(\neg P)]_{\bowtie p}$
Before R: $[\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P)))]_{\bowtie p}$
After Q: $[\Box (Q \rightarrow \Box^{[t1,t2]}\;(\neg P))]_{\bowtie p}$
Between Q and R: $[\Box((Q \; \wedge \; \Box^{[0,t1]} (\neg R) \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee (\Box^{[t1,t2]} (\neg P))]_{\bowtie p}$
After Q until R: $[\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow (\neg P \; \mathcal{W}^{[t1,t2]} \;R))]_{\bowtie p}$
CSL Globally: $\mathcal{P}_{\bowtie p}(\Box^{[t1,t2]}\;(\neg P))$
Before R: $\mathcal{P}_{\bowtie p} (\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee \mathcal{P}_{=1}(\Box^{[t1,t2]} (\neg P))))$
After Q: $\mathcal{P}_{=1} (\Box (Q \rightarrow \mathcal{P}_{\bowtie p} (\Box\;^{[t1,t2]}\;(\neg P))))$
Between Q and R: $\mathcal{P}_{=1} (\Box ((Q \; \wedge \; \mathcal{P}_{=1} (\Box^{[0,t1]} (\neg R))) \rightarrow\mathcal{P}_{\bowtie p} (\Diamond^{[t1,\infty)} R \rightarrow ((\neg P \; \; \mathcal{U}^{[t1,t2]} \; R) \vee \mathcal{P}_{=1}(\Box^{[t1,t2]} (\neg P))))$
After Q until R: $\mathcal{P}_{=1} (\Box ((Q\; \wedge \;\mathcal{P}_{=1}(\Box^{[0,t1]} (\neg R))) \rightarrow \mathcal{P}_{\bowtie p}(\neg P \; \mathcal{W}^{[t1,t2]} \;R)))$
Example and Known Uses
The probability that the system is free of failures in 2 time units is 0.98.
Additional notes
This pattern is the extension of the Absence pattern. This pattern can be considered the dual of the Probabilistic Invariance pattern proposed in [2].

Bibliography
1. Matthew B. Dwyer; George S. Avrunin; James C. Corbett, Patterns in Property Specifications for Finite-State Verification. ICSE 1999. pp. 411-420.
2. Lars Grunske, Specification patterns for probabilistic quality properties. ICSE 2008. pp. 31-40.

Home page

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