## 3 Property Patterns Based on Timed Automata  
A pattern can give a general way of solving one kind of problem. Since modeling properties that the system needs to satisfy is a necessary step, we need to explore the patterns of the verification properties. Property patterns in previous works can infer the occurrence and sequence of events (e.g., the occurrence of event \(a\) must follow event \(b\)) and can also describe the logical behaviors of time-related events. On this basis, we propose common property patterns represented by timed automata. The property patterns are shown in the following figures. In the figures, \(a\), \(b\), \(c\) are all the events, \(x\) is a clock and \(k\) is any non-negative integer. The property patterns only have one clock. We can use a single pattern or a combination of multiple patterns to model a property, which may have multiple clocks. The property patterns are described one by one as follows. * **Name of property pattern:**_Absence_ **Problem to be solved:** An event must not occur within a certain amount of time. **Solution:** The patterns _Absence-1_ and _Absence-2_ are shown in Figure 2. For the self-transition in _Absence-1_, there is a clock constraint \(x>k\) which means that event \(a\) can only occur after \(k\) time units. The difference between _Absence-2_ and _Absence-1_ is whether the clock \(x\) is reset on the self-transition, which means that the time between two occurrences of event \(a\) must be larger than \(k\) time units. Event \(a\) may occur many times and also may never occur because there is no state invariant on \(State_{1}\) or \(State_{2}\). * **Name of property pattern:**_Existence_ **Problem to be solved:** An event must occur within a certain amount of time. **Solution:** The patterns _Existence-1_, _Existence-2_ and _Existence-3_ are shown in Figure 3. Due to the state invariant \(x\leq k\) on the states and the clock constraint \(x\leq k\) on the transitions, we can make sure that event \(a\) occurs within \(k\) time units. _Existence-1_ indicates that event \(a\) can occur many times and the time between two successive occurrences must be within \(k\) time units due to the resetting of the clock \(x\). In the patterns _Existence-2_ and _Existence-3_, the first occurrence of event \(a\) must be within \(k\) time units. Event \(a\) only occurs once within \(k\) time units in _Existence-2_, while it can happen many time in _Existence-3_ after the first occurrence. * **Name of property pattern:**_Response_ **Problem to be solved:** An event must always be followed by another event within a certain amount of time. **Solution:** The patterns _Response-1_ and _Response-2_ are shown in Figure 4. The state invariant \(x\leq k\) on the states and the clock constraint \(x\leq k\) on the transitions denotes the inevitability of the situation that event \(b\) follows event \(a\) within \(k\) time units. In addition, _Response-1_ indicates that event \(b\) can only occur after event \(a\), while the self-transition on \(State_{3}\) in _Response-2_ indicates that even if the event \(a\) does not occur, event \(b\) can occur separately. Figure 3: Property pattern of Existence. Figure 2: Property pattern of Absence. * **Name of property pattern:**_Precedence_ **Problem to be solved:*
* An event must always be preceded by another event within a certain amount of time. **Solution:*
* The patterns _Precedence-1_, _Precedence-2_, _Precedence-3_ and _Precedence-4_ are shown in Figure 5. _Precedence-1_ denotes that when event \(a\) occurs, the clock \(x\) is reset to zero. After that, if event \(b\) occurs, it must not be within \(k\) clock units, during which event \(a\) may continue to happen multiple times because of the self-transition on \(State_{2}\). _Precedence-2_ denotes that after event \(a\), if event \(b\) occurs, it must be within \(k\) time units, during which event \(a\) can also occur many times. _Precedence-3_ and _Precedence-4_ are similar to the above.