Response Invariance Property Pattern
Untimed version
| Pattern Name and Classification | ||
| Response Invariance : Order Specification Pattern | ||
| Structured English Specification | ||
| Scope, if P [has occurred], then in response S holds continually. | ||
| Pattern Intent | ||
| To describe cause-effect relationships between a pair of events/states. An occurrence of the first, the cause $P$, must be followed by an invariant occurrence of the second, the effect $S$. | ||
| Temporal Logic Mappings | ||
| LTL | Globally: | $\Box \; (P \;\rightarrow \; \Box\; S)$ |
| Before R: | $\Diamond \; R \;\rightarrow \; (P \;\rightarrow \; (\Box\; (S \wedge \neg R))) \; \mathcal{U} \; R$ | |
| After Q: | $\Box(Q \;\rightarrow \; \Box(P \;\rightarrow \; \Box \; S))$ | |
| Between Q and R: | $\Box((Q \;\wedge \neg R \;\wedge \Diamond \; R) \;\rightarrow \; (P \;\rightarrow \; (\Box \; (S \;\wedge \neg R))) \; \mathcal{U} \; R)$ | |
| After Q until R: | $\Box(Q \;\wedge \neg R \;\rightarrow \; ((P \;\rightarrow \; (\Box \; (S \;\wedge \neg R))) \; \mathcal{W} \; R)$ | |
| CTL | Globally: | $AG(P \;\rightarrow \; AG(S))]$ |
| Before R: | $A[((P \;\rightarrow \; AG \; (S \& !R)) \vee AG(\neg R)) \; \mathcal{W} \; R]$ | |
| After Q: | $A[!Q \;\mathcal{W} \; (Q \& AG(P \;\rightarrow \; AG(S))]$ | |
| Between Q and R: | $AG(Q \& \neg R \;\rightarrow \; A[((P \;\rightarrow \; AG \; (S \& \neg R)) \vee AG(\neg R)) \; \mathcal{W} \; R])$ | |
| After Q until R: | $AG(Q \& \neg R \;\rightarrow \; A[(P \;\rightarrow \; AG \; (S \& \neg R)) \; \mathcal{W} \; R])$ | |
| Example and Known Uses | ||
| After a write operation, the memory location should retain the data | ||
| Relationships | ||
| This pattern is closely related (it is an extension) to the Response Pattern(Untime version). | ||
Time constrained version
The Response Invariance Property Pattern has been proposed in [2].
Probabilistic version
| Pattern Name and Classification | ||
| Probabilistic Response Invariance : Probabilistic Order Specification Pattern | ||
| Structured English Specification | ||
| Scope, if P [has occurred], then in response S holds [within Time(0)] continually [with ProbabilityBound]. | ||
| Pattern Intent | ||
| To describe cause-effect relationships between a pair of events/states. An occurrence of the first, the cause $P$, must be followed by an invariant occurrence of the second, the effect $S$ within a timebound and with a certain probability bound $\bowtie p$. | ||
| Temporal Logic Mappings | ||
| PLTL | Globally: | $[\Box \; (P \;\rightarrow \; \Box^{[ t_1, t_2]} \; S)]_{\bowtie p}$ |
| Before R: | $[\Diamond^{[ t_1, \infty)} \; R \;\rightarrow \;( (P \;\rightarrow \; (\Box^{[ t_1, t_2]} \; (S \wedge \neg R))) \; \mathcal{U} \; R)]_{\bowtie p}$ | |
| After Q: | $[\Box(Q \;\rightarrow \; \Box(P \;\rightarrow \; \Box^{[ t_1, t_2]} \; S))]_{\bowtie p}$ | |
| Between Q and R: | $[\Box((Q \;\wedge \Box^{[ 0, t_1]}\neg R \;\wedge \Diamond^{[ t_1, \infty)} \; R) \;\rightarrow \; (P \;\rightarrow \; (\Box^{[ t_1, t_2]} \; (S \;\wedge \neg R))) \; \mathcal{U} \; R)]_{\bowtie p}$ | |
| After Q until R: | $[\Box((Q \;\wedge \Box^{[ 0, t_1]} \neg R) \;\rightarrow \; ((P \;\rightarrow \; (\Box^{[ t_1, t_2]} \; (S \;\wedge \neg R))) \; \mathcal{W} \; R)]_{\bowtie p}$ | |
| TCTL | Globally: | $\mathcal{P}_{=1} (\Box(P \;\rightarrow \; \mathcal{P}_{\bowtie p}(\Box^{[ t_1, t_2]} (S))))$ |
| Before R: | $\mathcal{P}_{=1}[(P \;\rightarrow \; (\mathcal{P}_{\bowtie p}(\Box^{[ t_1, t_2]} \; (S \wedge \neg R))) \vee \mathcal{P}_{=1}(\Box(\neg R))) \; \mathcal{W} \; R]$ | |
| After Q: | $\mathcal{P}_{=1}[\neg Q \; \mathcal{W} \; (Q \wedge \mathcal{P}_{=1}(\Box(P \;\rightarrow \; \mathcal{P}_{\bowtie p}(\Box^{[ t_1, t_2]}(S))))]$ | |
| Between Q and R: | $\mathcal{P}_{=1}(\Box(Q \wedge \mathcal{P}_{=1}(\Box^{[0, t_1]}(\neg R)) \;\rightarrow \; \mathcal{P}_{=1}[((P \;\rightarrow \; \mathcal{P}_{\bowtie p}(\Box^{[ t_1, t_2]} \; (S \wedge \neg R))) \vee \mathcal{P}_{=1}(\Box(\neg R))) \; \mathcal{W} \; R]))$ | |
| After Q until R: | $\mathcal{P}_{=1}(\Box(Q \wedge \mathcal{P}_{=1}(\Box^{[0, t_1]}\neg R) \;\rightarrow \; \mathcal{P}_{=1}[(P \;\rightarrow \; \mathcal{P}_{\bowtie p}(\Box^{[ t_1, t_2]} \; (S \wedge \neg R)]) \; \mathcal{W} \; R]))$ | |
| Example and Known Uses | ||
| After a write operation, the memory location should retain the data for the next 3 years with a probability of 99.9%. | ||
| Relationships | ||
| This pattern is closely related (it is an extension) to the Response Pattern(Probabilistic version). | ||
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. Sascha Konrad; Betty H.C. Cheng, Real-time specification patterns.ICSE 2005. pp. 372-381.
3. Holzmann, Gerard J.The Spin Model Checker: Primer and Reference Manual.Addison Wesley Publishing Company, 2003.