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