Until Property Pattern
Untimed version
| Pattern Name and Classification | ||
| Until: Order Specification Pattern | ||
| Structured English Specification | ||
| Scope, P [holds] without interruption until S [holds]. | ||
| Pattern Intent | ||
| Until has been proposed by Grunske (2008) in [1] . This pattern describes a scenario in which an event/state will eventually become true, after another event/state held continuously. | ||
| Temporal Logic Mappings | ||
| LTL | Globally: | $P \; \mathcal{U} \; S$ |
| Before R: | $\Diamond R \rightarrow ( (P \wedge \neg R) \; \mathcal{U} \;(S \vee R))$ | |
| After Q: | $\Box (Q \rightarrow (P \; \mathcal{U}\;S)$ | |
| Between Q and R: | $\Box((Q \; \wedge \; \neg R \; \wedge \Diamond R) \rightarrow ((P \wedge \neg R) \; \mathcal{U} \;(S \wedge \neg R)))$ | |
| After Q until R: | $\Box ((Q \; \wedge \; (\neg R)) \rightarrow ((P \; \mathcal{U} \;S) \; \mathcal{W} \;R))$ | |
| CTL | Globally: | $A[P \; \mathcal{U} \;S]$ |
| Before R: | $A[A[P \; \mathcal{U} \;S] \; \mathcal{W} \;R]$ | |
| After Q: | $AG(Q \rightarrow \; A[P\; \mathcal{U} \;S])$ | |
| Between Q and R: | $AG((Q \; \wedge \;AG (\neg R)) \rightarrow A[A[P \; \mathcal{U} \;S] \; \mathcal{W} \; R)])$ | |
| After Q until R: | $AG((Q\; \wedge \;AG (\neg R)) \rightarrow A[A[P \; \mathcal{U} \;S] \; \mathcal{W} \;R])$ | |
| Example and Known Uses | ||
| Power to a system must be available until a shutdown command is issued. (scope: global; source: satellite control system) | ||
Time-constrained version:
| Pattern Name and Classification | ||
| Time-constrained Until: Real-time Order Specification Pattern | ||
| Structured English Specification | ||
| Scope, P [holds] without interruption until S [holds] [ Time(0)] | ||
| Pattern Intent | ||
| This pattern describes a scenario in which an event/state will eventually become true within a given time bound, after another event/state held continuously. | ||
| Temporal Logic Mappings | ||
| MTL | Globally: | $P \; \mathcal{U}^{[t1,t2]}\;S$ |
| Before R: | $\Diamond^{[t1,\infty)} R \rightarrow ( (P \wedge \neg R) \; \mathcal{U}^{[t1,t2]}\;(S \vee R))$ | |
| After Q: | $\Box (Q \rightarrow (P \; \mathcal{U}^{[t1,t2]}\;S)$ | |
| Between Q and R: | $\Box((Q \; \wedge \; \neg R \; \wedge \Diamond^{[t1,\infty)} R) \rightarrow ( (P \wedge \neg R) \; \mathcal{U}^{[t1,t2]}\;(S \vee R)))$ | |
| After Q until R: | $\Box ((Q \; \wedge \; \Box^{[0,t1]} (\neg R)) \rightarrow ((P \; \mathcal{U}^{[t1,t2]}\;S) \; \mathcal{W} \;R))$ | |
| TCTL | Globally: | $A[P \; \mathcal{U}^{[t1,t2]} \;S]$ |
| Before R: | $A[A[P \; \mathcal{U}^{[t1,t2]} \;S] \; \mathcal{W} \;R]$ | |
| After Q: | $AG(Q \rightarrow \; A[P\; \mathcal{U}^{[t1,t2]} \;S])$ | |
| Between Q and R: | $AG((Q \; \wedge \;AG^{[0,t1]} (\neg R)) \rightarrow A[A[P \; \mathcal{U}^{[t1,t2]} \;S] \mathcal{W} \; R)])$ | |
| After Q until R: | $AG((Q\; \wedge \;AG^{[0,t1]} (\neg R)) \rightarrow A[A[P \; \mathcal{U}^{[t1,t2]} \;S] \; \mathcal{W} \;R])$ | |
| Example and Known Uses | ||
| After 30 ms of continuously operating the pump engine must be stopped. Note: the engine is connected to a piston rod which sends forward a plunger in order to deliver the insulin to the body. (scope:global; source: insulin pump). | ||
| Relationships | ||
| This pattern is the extension of the untimed version Until. | ||
Probabilistic version:
The Until Property Pattern has been proposed by Grunske in [1] and it can be found on the ProProST webpage.
Bibliography
1. Lars Grunske Specification patterns for probabilistic quality properties. ICSE 2008: 31-40