Constrained Response Property Pattern
Untimed version
| Pattern Name and Classification | ||
| Response: Order Specification Pattern | ||
| Structured English Specification | ||
| Scope, if P [has occurred], then in response S eventually holds without $Z_S$ [holding] in between. | ||
| 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 occurrence of the second, the effect $S$. | ||
| Temporal Logic Mappings | ||
| LTL | Globally: | $\Box \; (P \;\rightarrow \; \neg Z_S \; \mathcal{U} \; S)$ |
| Before R: | $\Diamond \; R \;\rightarrow \; (P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U} \; (S \wedge \neg R))) \; \mathcal{U} \; R$ | |
| After Q: | $\Box(Q \;\rightarrow \; \Box(P \;\rightarrow \; \neg Z_S \; \mathcal{U} \; S))$ | |
| Between Q and R: | $\Box((Q \;\wedge \Box \neg R \;\wedge \Diamond \; R) \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \wedge \neg Z_S\mathcal{U} \; (S \;\wedge \neg R))) \; \mathcal{U} \; R)$ | |
| After Q until R: | $\Box(Q \;\wedge \Box \neg R \;\rightarrow \; ((P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U} \; (S \;\wedge \neg R))) \; \mathcal{W} \; R)$ | |
| CTL | Globally: | $AG(P \;\rightarrow \; A[!Z_S \; \mathcal{U} (S)])$ |
| Before R: | $A[(P \;\rightarrow \; (A[!R \& !Z_S\; \mathcal{U} \; (S \wedge \neg R)]) \vee AG(!R)) \; \mathcal{W} \; R]$ | |
| After Q: | $A[!Q \; \mathcal{W} \; (Q \wedge AG(P \;\rightarrow \; A[!Z_S\mathcal{U}(S)])]$ | |
| Between Q and R: | $AG(Q \wedge AG !R \;\rightarrow \; A[((P \;\rightarrow \; A[!R \& !Z_S\; \mathcal{U} \; (S \wedge !R)]) \vee AG(!R)) \; \mathcal{W} \; R])$ | |
| After Q until R: | $AG(Q \wedge \Box !R \;\rightarrow \; A[(P \;\rightarrow \; A[!R \& !Z_S\; \mathcal{U} \; (S \wedge !R)]) \; \mathcal{W} \; R])$ | |
| Additional notes | ||
| The Response Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found on the following webpage: Response Property Pattern . | ||
Time-constrained version
| Pattern Name and Classification | ||
| Time-constrained Response: Real-time Order Specification Pattern | ||
| Structured English Specification | ||
| Scope, if P [has occurred], then in response S eventually holds without $Z_S$ [holding] in between and within [ Time(0)]. | ||
| 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 occurrence of the second, the effect $S$ without $Z_S$ holding and within a timebound [t_1,t_2]. | ||
| Temporal Logic Mappings | ||
| MTL | Globally: | $\Box \; (P \;\rightarrow \; \neg Z_S \; \mathcal{U}^{[ t_1, t_2]} \; S)$ |
| Before R: | $\Diamond^{[ t_1, \infty)} \; R \;\rightarrow \; (P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R))) \; \mathcal{U} \; R$ | |
| After Q: | $\Box(Q \;\rightarrow \; \Box(P \;\rightarrow \; \neg Z_S \; \mathcal{U}^{[ t_1, t_2]} \; S))$ | |
| Between Q and R: | $\Box((Q \;\wedge \Box^{[ 0, t_1]}\neg R \;\wedge \Diamond^{[ t_1, \infty)} \; R) \;\rightarrow \; (P \;\rightarrow \; (\neg R \; \wedge \neg Z_S\mathcal{U}^{[ t_1, t_2]} \; (S \;\wedge \neg R))) \; \mathcal{U} \; R)$ | |
| After Q until R: | $\Box(Q \;\wedge \Box^{[ 0, t_1]} \neg R \;\rightarrow \; ((P \;\rightarrow \; (\neg R \wedge \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \;\wedge \neg R))) \; \mathcal{W} \; R)$ | |
| TCTL | Globally: | $AG(P \;\rightarrow \; A[\neg Z_S \; \mathcal{U}^{[ t_1, t_2]} (S)])$ |
| Before R: | $A[(P \;\rightarrow \; (A[\neg R \& \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R)]) \vee AG(\neg R)) \; \mathcal{W} \; R]$ | |
| After Q: | $A[\neg Q \; \mathcal{W} \; (Q \wedge AG(P \;\rightarrow \; \neg Z_S \; A[\mathcal{U}^{[ t_1, t_2]}(S)])]$ | |
| Between Q and R: | $AG(Q \wedge AG^{[0, t_1]}\neg R \;\rightarrow \; A[((P \;\rightarrow \; A[\neg R \& \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R)]) \vee AG(\neg R)) \; \mathcal{W} \; R])$ | |
| After Q until R: | $AG(Q \wedge \Box^{[0, t_1]}\neg R \;\rightarrow \; A[(P \;\rightarrow \; A[\neg R \& \neg Z_S\; \mathcal{U}^{[ t_1, t_2]} \; (S \wedge \neg R)]) \; \mathcal{W} \; R])$ | |
| Additional notes | ||
| The Time-constrained Response Property Pattern has been proposed by Cheng in [2], proposed as Bounded Response . | ||
Probabilistic version
The Response Property Pattern has been proposed by Grunske in [3] and it can be found on the following webpage: Probabilistic Response Pattern.
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. Lars Grunske, Specification patterns for probabilistic quality properties. ICSE 2008. pp. 31-40.