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.