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.