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