State based Specification Patterns for UPPAAL

Patterns

The following specification patterns follow a state-based formalism, that is, we specify properties in terms of states.

Occurrence patterns detail the circumstances for a given state to arise during system execution.

Order patterns describe the relative sequences in which multiple states can occur during system execution.

To enable the verification with UPPAAL, we use the observer or flag techniques (see discussion here).

For the observer technique, we adjust the system model to emit events when the system enters or leaves state X, that is, X_reached or X_left is respectively sent through broadcast channels to the observer.
An observer may have a local clock c.
For the flag technique, we adjust the system model by adding a global variable X_holds that is set to 1 when the system enters state X and that is set to 0 when the system leaves state X. Consequently, we can check whether X_holds == 1 or X_holds == 0 in a formula and especially in guards of the observers.
For the flag technique, we adjust the system model by adding a global variable X_held_once = 0 (i.e., it is initialized with 0) that is set to 1 iff state X has been reached. When leaving state X, the variable is not reset such that it provides information whether the state X has been reached once yet or not.

For each pattern for either the untimed or timed version, we consider five scopes.

	Pattern	Untimed	Timed
1	Absence	✓	✓
2	Universality	✓	✓
3	Existence	✓	✓
4	Bounded Existence	✓	N/A
5	Recurrence	✓	✓
6	Response	✓	✓
7	Minimum Duration	N/A	✓
8	Maximum Duration	N/A	✓
9	Until	✓	✓
10	Constrained Response	✓	✓
11	Response Chain: 1 stimulus - N responses	✓	✓
12	Response Chain: N stimuli - 1 response	✓	✓
13	Response Invariance	✓	✓
14	Constrained Response Chain: 1 stimulus - N responses	✓	✓
17	Constrained Response Chain: N stimuli - 1 response	✓	✓
16	Precedence	✓	N/A
17	Precedence Chain: N causes - 1 effect	✓	N/A
18	Precedence Chain: 1 cause - N effects	✓	N/A
19	Constrained Precedence Chain: N causes - 1 effect	✓	N/A
20	Constrained Precedence Chain: 1 cause - N effects	✓	N/A

Luca Aceto, Augusto Burgueño and Kim G. Larsen Model checking via reachability testing for timed automata. In: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg.
Luca Aceto, Patricia Bouyer, Augusto Burgueño, Kim G Larsen: The power of reachability testing for timed automata, Theoretical Computer Science, Volume 300, Issue 1, 2003, Pages 411-475.
Marco Autili, Lars Grunske, Markus Lumpe, Patrizio Pelliccione and Antony Tang: Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar. IEEE TSE Vol. 41, No. 7, 2015.
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett: Patterns in property specifications for finite-state verification. In International conference on Software engineering (ICSE '99). ACM, 411-420.
Volker Gruhn and Ralf Laue: Patterns for Timed Property Specifications. In Electronic Notes in Theoretical Computer Science 153 (2006) 117–133
Klaus Havelund, Kim Guldstrand Larsen, and Arne Skou: Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL. In Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, 277-298
Sascha Konrad and Betty H. C. Cheng. Real-time specification patterns. In ICSE'05. ACM, 372-381

Specification Pattern Catalogue for UPPAAL

Evaluation