Semantics
In the following we give a pseudo-formal semantics for UPPAAL. The
semantics defines a timed transition system (S, s0, →)
describing the behaviour of a network of extended timed automata. The
set of states S is defined as {(L, v) | v
⊨ Inv(L)}, where L is a location
vector, v is a function (called a valuation) mapping
integer variables and clocks to their values, and Inv is a
function mapping locations and location vectors to invariants. The
initial state s0 is the state where all processes are in the
initial location, all variables have their initial value, and all
clocks are zero. The transition relation, →, contains two kinds of
transitions: delay transitions and action transitions. We will
describe each type below.
Given a valuation v and an expression e, we say
that v satisfies e if e evaluates to non-zero
for the given valuation v.
Invalid Evaluations
If during a successor computation any expression evaluation is
invalid (consult the section on expressions for further details about
invalid evaluations), the verification is aborted.
Delay Transitions
Delay transitions model the passing of time without changing the
current location. We have a delay transition (L, v) −d→
(L, v'), where d is a non-negative real, if and only
if:
- v' = v+d, where v+d is obtained by
incrementing all clocks with d.
- for all 0 ≤ d' ≤ d: v+d' ⊨
Inv(L)
- L contains neither committed nor urgent locations
- for all locations ℓ in L and for all locations
ℓ' (not necessarily in L), if there is an edge from
ℓ to ℓ' then either:
- this edge does not synchronise over an urgent channel, or
- this edge does synchronise over an urgent channel, but for all
0 ≤ d' ≤ d we have that v+d' does not satisfy
the guard of the edge.
Action Transitions
For action transtions, the synchronisation label of edges is
important. Since UPPAAL supports arrays of channels, we have that the
label contains an expression evaluating to a channel. The concrete
channel depends on the current valuation. To avoid cluttering the
semantics we make the simplifying assumption that each
synchronisation label refers to a channel directly.
Priorities
increase the determinism of a system by letting a high priority
action transition block a lower priority action transition.
Note that delay transitions can never be blocked, and no
action transition can be blocked by a delay transition.
For action transitions, there are three cases: Internal
transitions, binary synchronisations and broadcast
synchronisations. Each will be described in the following.
Internal Transitions
We have a transition (L, v) −*→
(L', v') if there is an edge e=(ℓ,ℓ') such that:
- there is no synchronisation label on e
- v satisfies the guard of e
- L' = L[ℓ'/ℓ]
- v' is obtained from v by executing the update
label given on e
- v' satisfies Inv(L')
- Either ℓ is committed or no other location in L
is committed.
- There is no action transition from (L, v)
with a strictly higher priority.
Binary Synchronisations
We have a transition (L, v) −*→
(L', v') if there are two edges
e1=(ℓ1,ℓ1') and
e2=(ℓ2,ℓ2') in
two different processes such that:
- e1 has a synchronisation label c! and
e2 has a synchronisation label c?, where c
is a binary channel.
- v satisfies the guards of e1 and
e2.
- L' = L[ℓ1'/ℓ1, ℓ2'/ℓ2]
- v' is obtained from v by first executing the
update label given on e1 and then the update label given on
e2.
- v' satisfies Inv(L')
- Either
- ℓ1 or ℓ2 or both locations are committed, or
- no other location in L is committed.
- There is no action transition from (L, v)
with a strictly higher priority.
Broadcast Synchronisations
Assume an order p1, p2, … pn of processes given by the
order of the processes in the system declaration statement. We have a
transition (L, v) −*→ (L', v')
if there is an edge e=(ℓ,ℓ') and m
edges ei=(ℓi,ℓi')
for 1≤i≤m such that:
- Edges e, e1, e2, …, em are in different processes.
- e1, e2, …, em are ordered according to the process
ordering p1, p2,… pn.
- e has a synchronisation label c! and e1,
e2, …, em have synchronisation labels c?,
where c is a broadcast channel.
- v satisfies the guards of e, e1, e2,
… em.
- For all locations ℓ in L not a source of one of
the edges e, e1, e2, … em,
all edges from ℓ either do not have a synchronisation label
c? or v does not satisfy the guard on the edge.
- L' = L[ℓ'/ℓ, ℓ1'/ℓ1,
ℓ2'/ℓ2, … ℓm'/ℓm]
- v' is obtained from v by first executing the
update label given on e and then the update labels given on
ei for increasing order of i.
- v' satisfies Inv(L')
- Either
- one or more of the locations ℓ, ℓ1, ℓ2, … ℓm are
committed, or
- no other location in L is committed.
- There is no action transition from (L, v)
with a strictly higher priority.
Probabilistic Transitions
In statistical model checking
the concrete delay and transition are determined as follows:
- Each process chooses a delay based on its current location:
- If the current location invariant has a time bound, then the concrete
delay is taken according uniform distribution up to that bound.
- Otherwise (the time invariant is absent) the delay is chosen by
exponential distribution using the rate λ specified on the current
location. The probability density function of delay d∈[0;∞) is
F(d)=λe−λd, where e=2.718281828…
and the concrete delay is generated by
−ln(u)/λ where u is a uniform random
number from (0;1] interval.
- The process with the shortest delay is chosen. If there are several
such processes then a random one of these is chosen (according to uniform
distribution).
- The shortest delay is executed and continuous variables are updated.
- The chosen process attempts to take a transition:
- Compute all enabled internal and sending edge-transitions.
- Pick the concrete edge according to uniform distribution.
- If the edge has probabilistic branches, then the probability of taking
a branch i is determined by the ratio
wi/W, where wi
is the weight of the branch i and W is the sum of all
branch weights: W=Σjwj.
Statistical model checking has the following assumptions about the model:
- Input enableness (non-blocking inputs):
- Sending cannot be blocked, i.e. the channel is either broadcast or there is always one process with an enabled receiving edge-transition.
- Input determinism:
- There is exactly one enabled receiving edge-transition at a time. For binary synchronizations there is at most one receiving process at a time.
For more details about probabilistic semantics of priced timed automata please see:
Statistical Model Checking for Networks of Priced Timed Automata, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Jonas van Vliet and Zheng Wang. In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aalborg, Denmark, September 2011.