Constrained Response Chain Property Pattern
Constrained Response Chain Property Pattern: 1 stimulus 2 responses
The Constrained Response Chain Property Pattern: 1 stimulus 2 responses is a special case of the Constrained Response Chain Property Pattern: 1 stimulus N responses. The temporal logical formula for the 1-2 case can be derived by selecting the first (terminating) case for the extension ($Chain$)
Constrained Response Chain Property Pattern: 1 stimulus N responses
Untimed version (Constrained Response Chain 1-N)
| Pattern Name and Classification | |||
| Constrained Response Chain 1-N: Order Specification Pattern | |||
| Scope, if P [has occurred], then in response [without Constraint(0)] S eventually holds [<Chain>]. | <Chain>:= followed by T(i)[without Constraint(i)][<Chain>] | ||
| Pattern Intent | |||
| 1 stimulus -N responses constrained response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$ without $Z_S$ holding between the stimulus and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Base Formula | Extension |
| LTL | Globally: | $\Box (P \;\rightarrow \; (\neg Z_S \; \mathcal{U}\; (S [\wedge <Chain>])))$ | $<Chain>::= \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}\;(T_i [\wedge <Chain>]))$ |
| Before R: | $\Diamond R \;\rightarrow \; (P \;\rightarrow \; ((\neg R \; \wedge \; \neg Z_S) \; \mathcal{U} \; (S [\wedge <Chain>]))) U R$ | $<Chain>\; ::= \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge <Chain>] ))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \neg Z_S \; \mathcal{U} \; (S [\wedge <Chain>]\; ))))$ | $<Chain>\; ::= \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge <Chain>]))$ | |
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; ((\neg R\; \wedge \;\neg Z_S) \mathcal{U} (S \; [\wedge \; <Chain>] ))) U R)$ | $<Chain>\; ::= \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge <Chain>]))$ | |
| After Q until R: | $\Box (Q \;\rightarrow \; (P \;\rightarrow \; (( \neg R\; \wedge \; \neg Z_S) \mathcal{U} (S \; [\wedge \; <Chain>\;] ))) \mathcal{W} R )$ | $<Chain>\; ::= \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U} \;(T_i [\wedge <Chain>] ))$ | |
| CTL | Globally: | $AG(P \rightarrow A(!Z_S \mathcal{U}(S [\& <Chain>])))$ | $<Chain>\; ::= !Z_i \& AX(A(!Z_i \mathcal{U} (T_i [\& <Chain>])))$ |
| Before R: | N/A | N/A | |
| After Q: | N/A | N/A | |
| Between Q and R: | N/A | N/A | |
| After Q until R: | N/A | N/A | |
| Example and Known Uses | |||
| Example of original version of this pattern that does not contain time-constraints can be found in [http://patterns.projects.cis.ksu.edu/]. | |||
| Relationships | |||
| This pattern is closely related (it is an extension) to the Untimed version (Response Chain 1-N) pattern. | |||
| Syntax notes | |||
| The square brackets (as used in $[\wedge <Chain>]$) are used as a EBNF syntax construct to describe an optional extension. | |||
| Additional notes | |||
| The Constrained Response Chain Property Pattern has been proposed by Dwyer in [1]. | |||
Time constrained version (Constrained Response Chain 1-N)
| Pattern Name and Classification | |||
| Time-constrained Constrained Response Chain 1-N: Real-time Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if P [has occurred], then in response [within Time(0)][without Constraint(0)] S eventually holds [<Chain>]. | <Chain>:= followed by T(i)[within Time(i)][without Constraint(i)][<Chain>] | ||
| Pattern Intent | |||
| 1 stimulus -N responses constrained time-bounded response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$ within $t_0$ time units between the stimulus and the chain and within $t_1,..,t_n$ time units between the chain elements respectively and without $Z_S$ holding between the stimulus and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Base Formula | Extension |
| MTL | Globally: | $\Box (P \;\rightarrow \; (\neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>])))$ | $<Chain>\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>] ))$ |
| Before R: | $\Diamond R \;\rightarrow \; (P \;\rightarrow \; ((\neg R \; \wedge \; \neg Z_S) \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>]))) U R$ | $<Chain>\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>] ))))$ | $<Chain>\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; ((\neg R\; \wedge \;\neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) U R)$ | $<Chain>\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q until R: | $\Box (Q \;\rightarrow \; (P \;\rightarrow \; (( \neg R\; \wedge \; \neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) \mathcal{W} R )$ | $<Chain>\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| TCTL | Globally: | $AG(P \rightarrow A(\neg Z_S \mathcal{U}^{[0, t_0]}(S [\wedge <Chain>])))$ | $<Chain>\; ::= \neg Z_i \wedge AX(A( \neg Z_i \mathcal{U}^{[0, t_i]} (T_i [\wedge <Chain>])))$ |
| Before R: | N/A | N/A | |
| After Q: | N/A | N/A | |
| Between Q and R: | N/A | N/A | |
| After Q until R: | N/A | N/A | |
| Example and Known Uses | |||
| Cargo Smoke Controller: Stimulus - a cargo controller signals a smoke controller warning; Responses - (1) the air ventilation system is turned off and then (2) the compartment isolation valves are closed within 60 seconds; Constraint: recognized a false warning. | |||
| Relationships | |||
| This pattern is closely related (it is an extension) to the Time constrained version (Response Chain 1-N) pattern. | |||
| Syntax notes | |||
| The square brackets (as used in $[\wedge <Chain>]$) are used as a EBNF syntax construct to describe an optional extension. | |||
| Additional notes | |||
| The Constrained Response Chain Property Pattern has been proposed by Dwyer in [1]. The original version that does not contain time-constraints can be found in/as Untimed version. | |||
Probabilistic version (Constrained Response Chain 1-N)
| Pattern Name and Classification | |||
| Probabilistic Constrained Response Chain 1-N: Probabilistic Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if P [has occurred], then in response [within Time(0)][without Constraint(0)] S eventually holds [<Chain>] with [ProbabilityBound]. | <Chain>:= followed by T(i)[within Time(i)][without Constraint(i)][<Chain>] | ||
| Pattern Intent | |||
| 1 stimulus-N responses probabilistic time bounded constrained response chain: A system responds to a stimulus $P$ with a chain (of events) $S, T_1,T_2,.., T_n$ with a certain probability $_{\bowtie p}$ within $t_0$ time units between the stimulus and the chain and within $t_1,..,t_n$ time units between the chain elements respectively and without $Z_S$ holding between the stimulus and the chain and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Base Formula | Extension |
| PLTL | Globally: | $[\Box (P \;\rightarrow \; (\neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>])))]_{\bowtie p}$ | $<Chain>\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>] ))$ |
| Before R: | $[\Diamond R \;\rightarrow \; (P \;\rightarrow \; ((\neg R \; \wedge \; \neg Z_S) \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>]))) U R]_{\bowtie p}$ | $<Chain>\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q: | $[\Box (Q \;\rightarrow \; \Box (P \;\rightarrow \; ( \neg Z_S \; \mathcal{U}^{[0, t_0]} \; (S [\wedge <Chain>] ))))]_{\bowtie p}$ | $<Chain>\; := \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| Between Q and R: | $[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (P \;\rightarrow \; ((\neg R\; \wedge \;\neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) U R)]_{\bowtie p}$ | $<Chain>\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| After Q until R: | $[\Box (Q \;\rightarrow \; (P \;\rightarrow \; (( \neg R\; \wedge \; \neg Z_S) \mathcal{U}^{[0, t_0]} (S \; [\wedge \; <Chain>]))) \mathcal{W} R )]_{\bowtie p}$ | $<Chain>\; := \neg R \wedge \neg Z_i \wedge o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i [\wedge <Chain>]))$ | |
| CSL | Globally: | $\mathcal{P}_{=1} (\Box (P \rightarrow \mathcal{P}_{\bowtie p}(\neg Z_S \mathcal{U}^{[0, t_0]}(S [\wedge <Chain>]))))$ | $<Chain>\; ::= \neg Z_i \wedge \mathcal{P}_{=1}(o(\mathcal{P}_{=1}( \neg Z_i \mathcal{U}^{[0, t_i]} (T_i [\wedge <Chain>]))))$ |
| Before R: | N/A | N/A | |
| After Q: | N/A | N/A | |
| Between Q and R: | N/A | N/A | |
| After Q until R: | N/A | N/A | |
| Syntax notes | |||
| The square brackets (as used in $[\wedge <Chain>]$) are used as a EBNF syntax construct to describe an optional extension. | |||
| Relationships | |||
| This pattern is closely related (it is an extension) to the Probabilistic version (Response Chain 1-N) pattern. | |||
| Example and Known Uses | |||
| Cargo Smoke Controller: Stimulus - a cargo controller signals a smoke controller warning; Responses - (1) the air ventilation system is turned off and then (2) the compartment isolation valves are closed within 60 seconds with a probability of 99.99%; Constraint: recognized a false warning. | |||
Constrained Response Chain Property Pattern: N stimuli 1 response
Untimed version (Constrained Response Chain N-1)
| Pattern Name and Classification | |||
| Constrained Response Chain N-1: Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if S[<Chain>] [has occurred], then P eventually holds and without $Z_P$ holding between the stimulus and the chain | <Chain>:= followed by //T(i)[<Chain>] without $Z_i$ | ||
| Pattern Intent | |||
| N stimulus-1 responses constrained response chain: A system responds to a stimulus $S$ and a chain (of events) $T_1,T_2,.., T_n$ with a response P without $Z_P$ holding between the stimulus including the chain and the response, and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Base Formula | Extension |
| LTL | Globally: | $\Box (S \wedge o (\neg Z_1 \; \mathcal{U} (T _1 \wedge <Chain>)))$ | $<Chain>\; := o(\neg Z_i \; \mathcal{U} \;(T_i \wedge <Chain>)) \| o(\neg Z_i \; \mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ |
| Before R: | $\Diamond R \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}\; T_1 \wedge <Chain> )) \mathcal{U} R)$ | $<Chain>\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (S \wedge o (\neg Z_1 \; \mathcal{U} (T _1 \wedge <Chain>))))$ | $<Chain>\; := o(\neg Z_i \; \mathcal{U} \;(T_i \wedge <Chain>)) \| o(\neg Z_i \; \mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ | |
| Between Q and R: | $\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}\; (T_1 \wedge <Chain> ))) \mathcal{U} R))$ | $<Chain>\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ | |
| After Q and R: | $\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1) \;\mathcal{U}\; T_1 (\wedge <Chain> ))) \mathcal{W} R))$ | $<Chain>\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i )\;\mathcal{U} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ | |
| CTL | Globally: | N/A | N/A |
| Before R: | N/A | N/A | |
| After Q: | N/A | N/A | |
| Between Q and R: | N/A | N/A | |
| After Q until R: | N/A | N/A | |
| Relationships | |||
| This pattern is closely related (it is an extension) to the Response Pattern(Untimed version). | |||
| Syntax notes | |||
| The square brackets (as used in $[\wedge <Chain>]$) are used as a EBNF syntax construct to describe an optional extension. | |||
Time constrained version (Constrained Response Chain N-1)
| Pattern Name and Classification | |||
| Time-constrained Constrained Response Chain N-1: Real-time Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if S[<Chain>] [has occurred], then in response [within Time(0)] P eventually holds without $Z_P$ ever holding. | <Chain>:= followed by T(i) without $Z_i$[within Time(i)][<Chain>] | ||
| Pattern Intent | |||
| N stimulus-1 responses time bounded constrained response chain: A system responds to a stimulus $S$ and a chain (of events) $T_1,T_2,.., T_n$ with a response P within $t_0$ time units between the stimulus including the chain and the response, and within $t_1,..,t_n$ time units between the chain elements respectively and without $Z_P$ holding between the stimulus including the chain and the response, and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Base Formula | Extension |
| MTL | Globally: | $\Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge <Chain>)))$ | $<Chain>\; := o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ |
| Before R: | $\Diamond R \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; T_1 \wedge <Chain> )) \mathcal{U} R)$ | $<Chain>\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ | |
| After Q: | $\Box (Q \;\rightarrow \; \Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge <Chain>))))$ | $<Chain>\; := o(\neg Z_1 \; \mathcal{U} ^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ | |
| Between Q and R: | $\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; ( T_1 \wedge <Chain> ))) \mathcal{U} R))$ | $<Chain>\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i)\;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ | |
| After Q and R: | $\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge <Chain> ))) \mathcal{W} R))$ | $<Chain>\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i)\;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ | |
| TCTL | Globally: | N/A | N/A |
| Before R: | N/A | N/A | |
| After Q: | N/A | N/A | |
| Between Q and R: | N/A | N/A | |
| After Q until R: | N/A | N/A | |
| Syntax notes | |||
| The square brackets (as used in $[\wedge <Chain>]$) are used as a EBNF syntax construct to describe an optional extension. | |||
Probabilistic version (Constrained Response Chain N-1)
| Pattern Name and Classification | |||
| Probabilistic Constrained Response Chain N-1: Probabilistic Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if S[<Chain>] [has occurred], then in response [within Time(0)] P eventually holds without $Z_P$ ever holding with [ProbabilityBound]. | <Chain>:= followed by T(i) without $Z_i$[within Time(i)][<Chain>] | ||
| Pattern Intent | |||
| N stimulus-1 responses probabilistic time bounded constrained response chain: A system responds to a stimulus $S$ and a chain (of events) $T_1,T_2,.., T_n$ with a response P with a certain probability $_{\bowtie p}$ within $t_0$ time units between the stimulus including the chain and the response, and within $t_1,..,t_n$ time units between the chain elements respectively and without $Z_P$ holding between the stimulus including the chain and the response, and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Base Formula | Extension |
| PLTL | Globally: | $[\Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge <Chain>)))]_{\bowtie p}$ | $<Chain>\; := o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ |
| Before R: | $[\Diamond R \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; T_1 \wedge <Chain> )) \mathcal{U} R)]_{\bowtie p}$ | $<Chain>\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ | |
| After Q: | $[\Box (Q \;\rightarrow \; \Box (S \wedge o (\neg Z_1 \; \mathcal{U}^{[0, t_1]} (T _1 \wedge <Chain>))))]_{\bowtie p}$ | $<Chain>\; := o(\neg Z_i \; \mathcal{U} ^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o(\neg Z_i \; \mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U} P ))$ | |
| Between Q and R: | $[\Box ((Q \wedge \neg R \wedge\;\Diamond R) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge <Chain> ))) \mathcal{U} R))]_{\bowtie p}$ | $<Chain>\; := o((\neg R \wedge \neg Z_i) \; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i) \;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ | |
| After Q and R: | $[\Box ((Q \wedge \neg R ) \;\rightarrow \; ((S \wedge o((\neg R \wedge \neg Z_1)\;\mathcal{U}^{[0, t_1]}\; (T_1 \wedge <Chain> ))) \mathcal{W} R))]_{\bowtie p}$ | $<Chain>\; := o((\neg R \wedge \neg Z_i)\; \mathcal{U}^{[0, t_i]} \;(T_i \wedge <Chain>)) \| o((\neg R \wedge \neg Z_i)\;\mathcal{U}^{[0, t_i]} \;(T_i \;\rightarrow \neg Z_P \; \mathcal{U}^{[0, t_0]} P ))$ | |
| CSL | Globally: | N/A | N/A |
| Before R: | N/A | N/A | |
| After Q: | N/A | N/A | |
| Between Q and R: | N/A | N/A | |
| After Q until R: | N/A | N/A | |
| Syntax notes | |||
| The square brackets (as used in $[\wedge <Chain>]$) are used as a EBNF syntax construct to describe an optional extension. | |||
Constrained Response Chain Property Pattern: 2 stimuli 1 response
Untimed version (Constrained Response Chain 2-1)
| Pattern Name and Classification | |||
| Constrained Response Chain 2-1: Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if S followed by T [has occurred] [without Constraint(1)], then in response P eventually holds [without Constraint(0)]. | |||
| Pattern Intent | |||
| 2 stimuli -1 response constrained response chain: A system responds to a stimulus chain (of events) $S, T$ with $P$ without $Z_P$ holding between the chain and the response and without $Z_1$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Logical Formula | |
| LTL | Globally: | $\Box (S \wedge \neg Z_1 \wedge o (\neg Z_1 \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o( \neg Z_1 \mathcal{U}(T \wedge (\neg Z_P \mathcal{U} P))))$ | |
| Before R: | $\Diamond R \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) U (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) U (T \wedge (\neg Z_P U P)))) U R$ | ||
| After Q: | $\Box (Q \;\rightarrow \; \Box (S \wedge \neg Z_1 \wedge o(\neg Z_1 \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o(\neg Z_1 \mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P)))))$ | ||
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1)\mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P)))) U R)$ | ||
| After Q until R: | $\Box (Q \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \;o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P)))) U (R \vee \Box (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U} (T \wedge (\neg Z_P \mathcal{U} P))))))$ | ||
| CTL | Globally: | N/A | |
| Before R: | N/A | ||
| After Q: | N/A | ||
| Between Q and R: | N/A | ||
| After Q until R: | N/A | ||
| Example and Known Uses | |||
| Example of original version of this pattern that does not contain time-constraints can be found in [http://patterns.projects.cis.ksu.edu/]. | |||
| Relationships | |||
| This pattern is closely related (it is an extension) to the Untimed version (Response Chain N-1) pattern. | |||
| Additional notes | |||
| A generic formulation of the N-1 Constrained Response Chain similar to the 1-N Constrained Response Chain would require a simultaneous substitution of the extensions $<Chain>$ since in the N-1 Constrained Response Chain formula fragment are repeated multiple times. | |||
Time constrained version (Constrained Response Chain 2-1)
| Pattern Name and Classification | |||
| Time-constrained Constrained Response Chain 2-1: Real-time Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if S followed by T [has occurred] [within Time(1)] [without Constraint(1)], then in response P eventually holds [within Time(0)][without Constraint(1)]. | |||
| Pattern Intent | |||
| 2 stimuli -1 responses constrained time-bounded response chain: A system responds to a stimulus chain (of events) $S, T$ with $P$ with a within $t_0$ time units between the chain and the response and within $t_1$ time units between the chain elements respectively and without $Z_P$ holding between the chain and the response and without $Z_1$ holding between the elements of the chain. | |||
| Temporal Logic Mappings | |||
| Logic | Scope | Logical Formula | |
| MTL | Globally: | $\Box (S \wedge \neg Z_1 \wedge o (\neg Z_1 \mathcal{U}^{[0, t_0]} (T \wedge \neg Z_P)) \;\rightarrow \; o( \neg Z_1 \mathcal{U}^{[0, t_1]}(T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P))))$ | |
| Before R: | $\Diamond R \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) U<c_1 (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) U<c_1 (T \wedge (\neg Z_P U <c_0 P)))) U R$ | ||
| After Q: | $\Box (Q \;\rightarrow \; \Box (S \wedge \neg Z_1 \wedge o(\neg Z_1 \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o(\neg Z_1 \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))))$ | ||
| Between Q and R: | $\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1)\mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) U R)$ | ||
| After Q until R: | $\Box (Q \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) U (R \vee \Box (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P))))))$ | ||
| TCTL | Globally: | N/A | |
| Before R: | N/A | ||
| After Q: | N/A | ||
| Between Q and R: | N/A | ||
| After Q until R: | N/A | ||
| Example and Known Uses | |||
| TOLL Road Design: Stimuli - (1) a car is passing a gantry and (2) then the system detects a speed greater than 130km/h; Constraint: Without an OCR failure to recognize the number plate; Response -the image made by the camera is send to the operator within 1 second. | |||
| Relationships | |||
| This pattern is closely related (it is an extension) to the Time constrained version (Response Chain N-1) pattern. | |||
Probabilistic version (Constrained Response Chain 2-1)
| Pattern Name and Classification | |||
| Probabilistic Constrained Response Chain N-1: Probabilistic Order Specification Pattern | |||
| Structured English Specification | |||
| Scope, if S followed by T [has occurred] [within Time(1)] [without Constraint(1)], then in response P eventually holds [within Time(0)][without Constraint(0)] with [ProbabilityBound] | |||
| Pattern Intent | |||
| N stimuli-1 response probabilistic time bounded constrained response chain: A system responds to a stimulus chain (of events) $S, T_1,T_2,.., T_n$ with $P$ with a certain probability $_{\bowtie p}$ within $t_0$ time units between the chain and the response and within $t_1,..,t_n$ time units between the chain elements respectively and without $Z_P$ holding between the chain and the response and without $Z_1,Z_2,.., Z_n$ holding between the elements of the chain. | |||
| Logic | Scope | Logical Formula | |
| PLTL | Globally: | $[\Box (S \wedge \neg Z_1 \wedge o (\neg Z_1 \mathcal{U}^{[0, t_0]} (T \wedge \neg Z_P)) \;\rightarrow \; o( \neg Z_1 \mathcal{U}^{[0, t_1]}(T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P))))]_{\bowtie p}$ | |
| Before R: | $[\Diamond R \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) \mathcal{U} R]_{\bowtie p}$ | ||
| After Q: | $[\Box (Q \;\rightarrow \; \Box (S \wedge \neg Z_1 \wedge o(\neg Z_1 \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o(\neg Z_1 \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))))]_{\bowtie p}$ | ||
| Between Q and R: | $[\Box ((Q \wedge \Diamond R) \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1)\mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) U R)]_{\bowtie p}$ | ||
| After Q until R: | $[\Box (Q \;\rightarrow \; (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P)))) U (R \vee \Box (S \wedge \neg Z_1 \wedge o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge \neg Z_P)) \;\rightarrow \; o((\neg R \wedge \neg Z_1) \mathcal{U}^{[0, t_1]} (T \wedge (\neg Z_P \mathcal{U}^{[0, t_0]} P))))))]_{\bowtie p}$ | ||
| CSL | Globally: | N/A | |
| Before R: | N/A | ||
| After Q: | N/A | ||
| Between Q and R: | N/A | ||
| After Q until R: | N/A | ||
| Example and Known Uses | |||
| TOLL Road Design: Stimuli - (1) a car is passing a gantry and (2) then the system detects a speed greater than 130km/h; Constraint: Without an OCR failure to recognize the number plate; Response -the image made by the camera is send to the operator within 1 second with a probability of 99.99%. | |||
| Relationships | |||
| This pattern is closely related (it is an extension) to the Probabilistic version (Response Chain N-1) 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.