Alexandre David

UPPAAL

Verification Algorithm, Options & Patterns

Alexandre David

Aalborg University

„ UPPAAL

„

Modelling Language

„

Specification Language

„ UPPAAL Verification Algorithm

„

Symbolic exploration algorithm

„

Zones & DBMs

„ Verification Options

„ Modelling Patterns

Outline

Modelling and Specification Language

Modeling Language

„ Network of TA = instances of templates

„

argument const type expression

„

argument type& name

„ Types

„

built-in types: int , int[min,max] , bool , arrays

„

typedef struct { … } name

„

typedef built-in-type name

„ Functions

„

C-style syntax, no pointer but references OK.

„ Select

name : type

+scalar sets

Un-timed Example: Jugs

„ Scalable, compact, & readable model.

„

const int N = 2; typedef int[0,N-1] id_t;

„

Jugs have their own id.

„

Actions = functions.

„

Pour: from id to another k different from id .

Jugs

2 5

Actions:

•fill

•empty

•pour Goal: obtain 1 unit.

Jug(const id_t id)

Jugs cont.

„

Jug levels & capacities:

int level[N];

const int capa[N] = {2,5};

„

void empty(id_t i) { level[i]=0; }

„

void fill(id_t i) { level[i] = capa[i]; }

„

void pour(id_t i, id_t j)

{ int max = capa[j] - level[j];

int poured = level[i] <? max;

level[i] -= poured;

level[j] += poured;

}

„

Auto-instantiation: system Jug;

Train-Gate Crossing (Exercise)

River Crossing

Stopable Area

[10,20]

[7,15]

[3,5]

Train-Gate Modeling

„ Scale the model:

„

const int N = 6; typedef int[0,N-1] id_t;

„ Trains have their local clocks.

„ The gate has its local list & functions.

Train(const id_t id) N trains...

Gate

controller

list

dequeue() front()

Communication via channels.

chan appr[N], stop[N], leave[N];

urgent chan go[N];

Train-Gate Crossing

River Crossing

Stopable Area

[10,20]

[7,15]

[3,5]

appr[id]! leave[id]!

stop[id]? go[id]?

Scalar Sets

„ Use: typedef scalar[N] setA;

„

defines a set of N scalars,

„

typedef scalar[N] setB;

defines another set of N scalars,

„

it is very important to use the typedef.

„

chan a[setA]; is an array of channels ranging over a scalar set – similarly for other types.

„

limited operations to keep scalars symmetric.

„ A way to specify symmetries in the model.

„

UPPAAL uses symmetry reduction automatically.

„

Reduction: Project the current state to a representative of

its equivalence class (w.r.t. symmetry).

Stop-Watches

„ It is possible to stop clocks.

„ In invariant expressions (conjunction of clock constraints), you can conjunct with:

„

expr ₁ ’ == expr ₂

expr ₁ evaluates to a clock expr ₂ evaluates to 0 or 1

„

available with forall(var:range) expr

„

The verification is then an over-approximation.

Exact model-checking problem is undecidable.

Logical Specifications

„

Validation Properties

„

Possibly: E<> P

„

Safety Properties

„

Invariant: A[] P

„

Pos. Inv.:E[] P

„

Liveness Properties

„

Eventually: A<> P

„

Leadsto: P Æ Q

„

Bounded Liveness

The expressions P and Q must be type safe, side effect free, and evaluate to a boolean.

Only references to integer variables,

constants, clocks, and

locations are allowed

(and arrays of these).

Logical Specifications

„

Validation Properties

„

Possibly: E<> P

„

Safety Properties

„

Invariant: A[] P

„

Pos. Inv.:E[] P

„

Liveness Properties

„

Eventually: A<> P

„

Leadsto: P Æ Q

„

Bounded Liveness

„

Leads to within: P Æ

Q

Logical Specifications

„

Validation Properties

„

Possibly: E<> P

„

Safety Properties

„

Invariant: A[] P

„

Pos. Inv.:E[] P

„

Liveness Properties

„

Eventually: A<> P

„

Leadsto: P Æ Q

„

Bounded Liveness

Logical Specifications

„

Validation Properties

„

Possibly: E<> P

„

Safety Properties

„

Invariant: A[] P

„

Pos. Inv.:E[] P

„

Liveness Properties

„

Eventually: A<> P

„

Leadsto: P Æ Q

„

Bounded Liveness

„

Leads to within: P Æ

Q

Logical Specifications

„

Validation Properties

„

Possibly: E<> P

„

Safety Properties

„

Invariant: A[] P

„

Pos. Inv.:E[] P

„

Liveness Properties

„

Eventually: A<> P

„

Leadsto: P Æ Q

„

Bounded Liveness

≤ t

≤ t

Jug Example

„ Safety: Never overflow.

„

A[] forall(i:id_t) level[i] <= capa[i]

„ Validation/Reachability: How to get 1 unit.

„

E<> exists(i:id_t) level[i] == 1

Train-Gate Crossing

„ Safety: One train crossing.

„

A[] forall (i : id_t) forall (j : id_t)

Train(i).Cross && Train(j).Cross imply i == j

„ Liveness: Approaching trains eventually cross.

„

Train(0).Appr --> Train(0).Cross

„

Train(1).Appr --> Train(1).Cross

„

…

„ No deadlock.

Verification Algorithm

Overview

„ Zones and DBMs

„ Reachability algorithm revisited

„ Minimal Constraint Form

„ Clock Difference Diagrams

„ Distributed UPPAAL [CAV2000, STTT2004]

„ Unification & Sharing [FTRTFT2002, SPIN2003]

„ Acceleration [FORMATS2002]

„ Static Guard Analysis [TACAS2003,TACAS2004]

„ Storage-Strategies ^[CAV2003]

State

(n, x=3.2, y=2.5 )

x y

x y

Symbolic state (set)

Zone:

conjunction of x-y<=n,

x<=n, x>=n

(n, 1 ≤ x ≤ 4, 1 ≤ y ≤ 3)

Zones

From infinite to finite

Zone=convex union of regions

→ more efficient

→ extrapolation

→ not always exact

Zones = Conjunction of Constraints

„ A zone Z is a conjunctive formula:

g ₁ & g ₂ & ... & g _n

where ^g _i is a clock constraint ^x _i ^{~ b} _i or ^x _i ^-x _j ^~b _ij

„ Use a zero-clock ^x ₀ (constant 0)

„ A zone can be re-written as a set:

{x _i -x _j ~ b _ij | ~ is < or ≤, i,j≤n}

„ This can be represented as a matrix, DBM

(Difference Bound Matrices)

Operations on Zones

„ Future delay Z↑:

[Z↑] = {u+d| d ∈ R, u∈[Z]}

„ Past delay Z↓:

[Z↓] = {u| u+d∈[Z] for some d∈R}

„ Reset: {x}Z or Z(x:=0)

[{x}Z] = {u[0/x] | u ∈[Z]}

„ Conjunction

[Z&g]= [Z]∩[g]

Theorem

„ The set of zones is closed under all constraint operations.

„ That is, the result of the operations on a zone is a zone.

„ That is, there will be a zone (a finite object i.e a zone/constraints) to represent the sets:

[Z↑], [Z↓], [{x}Z], [Z&g].

Symbolic Transitions

n

m x>3

y:=0

delays to

conjuncts to

projects to x

y

1 ≤ x ≤ 4 1 ≤ y ≤ 3

x

y ¹ _-2 ^≤ _≤ ^{x, 1} _x-y ^≤ _≤ ^y ₃

x

y 3 < x, 1 ≤ y -2 ≤ x-y ≤ 3

3 < x, y=0

x y

Thus (n, 1 ≤ x ≤ 4, 1 ≤ y ≤ 3) → ^a (m,3 < x, y=0)

Thus (n, 1 ≤ x ≤ 4, 1 ≤ y ≤ 3) → ^a (m,3 < x, y=0)

a

Symbolic Exploration

Reachable?

x

y

Symbolic Exploration

Reachable?

x y

Delay

Symbolic Exploration

Reachable?

x y

Left

Symbolic Exploration

Reachable?

x y

Left

Symbolic Exploration

Reachable?

x y

Delay

Symbolic Exploration

Reachable?

x y

Left

Symbolic Exploration

Reachable?

x y

Left

Symbolic Exploration

Reachable?

x y

Delay

Symbolic Exploration

Reachable?

x y

Down

Forward Reachability Algorithm

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed UNTIL Waiting = Ø

return false Init -> Final ?

PW

Forward Reachability Algorithm

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed UNTIL Waiting = Ø

return false Init -> Final ?

PW

Forward Reachability Algorithm

Passed Waiting

Final?

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed UNTIL Waiting = Ø

return false Init -> Final ?

PW

Forward Reachability Algorithm

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed UNTIL Waiting = Ø

return false Init -> Final ?

PW

Forward Reachability Algorithm

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed UNTIL Waiting = Ø

return false Init -> Final ?

PW

Forward Reachability Algorithm

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed

UNTIL Waiting = Ø return false

Init -> Final ?

PW

Forward Reachability Algorithm

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed

UNTIL Waiting = Ø return false

Init -> Final ?

PW

Difference Bound Matrices

x ₂ -x ₂ <=0 x ₂ -x ₁ <=1

x ₂ -x ₀ <=5

x ₁ -x ₂ <=3 x ₁ -x ₁ <=0

x ₁ -x ₀ <=6

x ₀ -x ₂ <=-1 x ₀ -x ₁ <=-2

x ₀ -x ₀ <=0

x _i -x _j <=c _ij

x

x

Zone

Difference Bound Matrices

x ₂ -x ₂ <=0 x ₂ -x ₁ <=3

x ₂ -x ₀ <=5

x ₁ -x ₂ <=3 x ₁ -x ₁ <=0

x ₁ -x ₀ <=6

x ₀ -x ₂ <=-1 x ₀ -x ₁ <=-2

x ₀ -x ₀ <=0

x _i -x _j <=c _ij

x

x

Canonical representation:

All constraints as tight as possible.

Needed for inclusion checking.

→ Unique DBM to represent a zone.

x

-x

<=5 ?

x

-x

<=4 ?

Bellman 1958, Dill 1989

x<=1 y-x<=2 z-y<=2 z<=9 x<=1 y-x<=2 z-y<=2 z<=9

x<=2 y-x<=3 y<=3 z-y<=3 z<=7 x<=2 y-x<=3 y<=3 z-y<=3 z<=7

D1

D2

How to check for inclusion?

0

x

y z

1 2

9 2

0

x

y z

2 3

7 3

3

? ?

Graph

Graph

⊆

Why to Make DBMs Canonical?

x<=1 y-x<=2 z-y<=2 z<=9 x<=1 y-x<=2 z-y<=2 z<=9

x<=2 y-x<=3 y<=3 z-y<=3 z<=7 x<=2 y-x<=3 y<=3 z-y<=3 z<=7

D1

D2

How to check for inclusion?

0

x

y z

1 2

9 2

Shortest Paths Closure

Shortest Paths Closure

0

x

y z

1 2

5 2

0

x

y z

2 3

7 3

0

x

y z

2 3

6 3

3

3 3

Graph

Graph

? ⊆ ?

4

6

Why to Make DBMs Canonical?

x<=1 y>=5 y-x<=3 x<=1 y>=5 y-x<=3

D

0

y x

1 3

-5

Negative Cycle iff

empty solution set

Graph

<0

<0

<0

After the “closure”

algorithm: one <0 in the diagonal.

Empty Zones/DBMs?

Constraint Implementation

„ Array of integers with a special encoding:

„

r = (bound << 1) | weak

„

bound and weakness of the constraint encoded as one integer

„

encoding preserves order of constraints

„

addition (useful for shortest paths closure):

r ₁ ⊕r ₂ = ∞ if r ₁ = ∞ or r ₂ = ∞

r ₁ ⊕r ₂ = r ₁ +r ₂ -((r ₁ | r ₂ ) & 1) otherwise

Canonical Form Algorithm

Floyd’s All Two Pairs Shortest Paths

proc close(D)

for k = 1 to n do for i = 1 to n do

for j = 1 to n do

D _ij = min(D _ij , D _ik ⊕ D _kj ) proc closek(D)

for i = 1 to n do for j = 1 to n do

D _ij = min(D _ij , D _ik ⊕ D _kj )

Inclusion Relation Algorithm

const DIFFERENT = 0 const SUBSET = 1

const SUPERSET = 2 const EQUAL = 3

function check(A,B) sub = 1

sup = 1

for i = 1 to n do for j = 1 to n do

sub &= A _ij ≤ B _ij sup &= A _ij ≥ B _ij

return sub | (sup << 1)

1<= x <=4 1<= y <=3 1<= x <=4 1<= y <=3

D x

y

x y

Future D

0

y 4 x

-1 3 -1

Shortest Paths Closure

Remove upper bounds on clocks

1<=x, 1<=y -2<=x-y<=3 1<=x, 1<=y -2<=x-y<=3

y x -1

-1

3 2

0

y x -1

-1

3 2

0

4 3

0 0

0

∞

∞

Future Operation

Future - Algorithm

proc future(A)

for i = 1 to n do A _i1 = ∞

Important property:

If A is canonical then A stays canonical!

x y

D

1<=x, 1<=y -2<=x-y<=3 1<=x, 1<=y -2<=x-y<=3

y x -1

-1

3 2

0

Remove all bounds involving y and set y to 0

x y

{y}D

y=0, 1<=x y=0, 1<=x

y x -1

0

0 ₀

Reset Operation

Projection

Reset - Algorithm

proc reset(A,x) A _1x = (0,≤)

A _x1 = (0,≤)

This does not preserve canonicity.

We need to “close” the DBM, which costs n ³ in time.

Reset – Revised Algorithm

proc reset(A,x,m) for i = 1 to n do

A _xi = (m,≤) ⊕ A _1i A _ix = A _i1 ⊕ (-m,≤)

This preserves canonicity.

It is cheaper to keep canonicity than

to “close” a DBM when needed.

Tightening - Algorithm

proc tighten(D,x,y,c) if D _yx ⊕ c < 0 then

D ₁₁ = (-1,≤) else D _xy = c

closek(D,x) closek(D,y) fi

This preserves canonicity.

x1-x2<=4 x2-x1<=10 x3-x1<=2 x2-x3<=2 x0-x1<=3 x3-x0<=5 x1-x2<=4 x2-x1<=10 x3-x1<=2 x2-x3<=2 x0-x1<=3 x3-x0<=5

x1 x2

x3 x0

-4

10 2 2

5 3

x1 x2

x3 x0

-4

4

2 2

5

3 3 -2 -2

1 Shortest

Closure Path O(n^3)

Space n^2

Improving Space Consumption

x1-x2<=4 x2-x1<=10 x3-x1<=2 x2-x3<=2 x0-x1<=3 x3-x0<=5 x1-x2<=4 x2-x1<=10 x3-x1<=2 x2-x3<=2 x0-x1<=3 x3-x0<=5

x1 x2

x3 x0

-4

10 2 2

5 3

x1 x2

x3 x0

-4

4

2 2

5 3

x1 x2

x3 x0

-4

2 2 3

3 -2 -2

1

Shortest Paths Closure O(n^3)

Shortest Paths Reduction

O(n^3) ₃

Space worst O(n^2) practice O(n)

RTSS 1997

Large gain in space.

Small price in time.

Improving Space Consumption

G: weighted graph

Minimal Graph

1. Equivalence classes based on 0-cycles.

G: weighted graph

Minimal Graph

1. Equivalence classes based on 0-cycles.

2. Graph based on representatives.

Safe to remove redundant edges

G: weighted graph

Minimal Graph

1. Equivalence classes based on 0-cycles.

2. Graph based on representatives.

Safe to remove redundant edges 3. Shortest Path Reduction

=

One cycle pr. class +

Removal of redundant edges between classes

G: weighted graph

Given some canonical order of clocks

Minimal Graph

Earlier Termination

Passed

Waiting Final

Init

INITIAL Passed := Ø;

Waiting := {(n

,Z

)}

REPEAT

pick (n,Z) in Waiting

if (n,Z) = Final return true for all (n,Z)→(n’,Z’):

if for some (n’,Z’’) Z’⊆ Z’’ continue else add (n’,Z’) to Waiting

move (n,Z) to Passed

UNTIL Waiting = Ø return false

Init -> Final ? PW

(n’,Z’)⊆PW

Clock Difference Diagrams

= Binary Decision Diagrams + Difference Bounded Matrices

CDD-representations CDD-representations

CAV99

„

Nodes labeled with differences

„

Maximal sharing of

substructures (also across different CDDs)

„

Maximal intervals

„

Linear-time algorithms for set-theoretic operations.

„

NDD’s Maler et. al

„

DDD’s Møller, Lichtenberg

„

Past experiments showed

gains in time & space.

Verification Options

Verification Options

Search Order

Depth First Breadth First State Space Reduction

None

Conservative Aggressive

State Space Representation DBM

Compact Form

Under Approximation Over Approximation Diagnostic Trace

Some

Shortest

Fastest

However,

Passed list useful for efficiency

State Space Reduction

Cycles:

Only symbolic states

involving loop-entry points

need to be saved on Passed list

State Space Reduction

To Store or Not To Store

Audio Protocol 117 states

!

81 states

! 9 states

Behrmann, Larsen, Pelanek 2003

Time OH

less than 10%

x y

Convex Hull

1 3 5

1 3 5

TACAS04: An EXACT method performing as well as Convex Hull has been

developed based on abstractions taking max constants into account.

Over-Approximation

Convex Hull

Passed

Waiting Final

Init PW

Under-Approximation

Bitstate Hashing

Passed

Waiting Final

Init

PW 1

0 1 0

0 1 Hash function

1 bit per passed state Under-approx.

Several states may collide on the same bit.

Inclusion check only with waiting states.

“Equality” with passed.

Bit Array

Under-Approximation

Bitstate Hashing

Modelling Patterns

Variable Reduction

„ Reduce size of state space by explicitly resetting variables when they are not used!

„ Automatically

performed for clock

variables (active clock

reduction)

x is only active in location S1

x>3 x<5

x:=0 x:=0

S x is inactive at S if on all path from S, x is always reset before being tested.

Definition

x<7

Clock Reduction (Automatic)

Synchronous Value Passing

Atomicity

„ Loops & complex control structures:

C-functions.

„ To allow encoding of multicasting.

„ Committed locations.

Bounded Liveness

„ Leads to within: φ Æ _≤t ψ

„

More efficient than leadsto:

φ leadsto _≤t ψ reduced to A□(b⇒z ≤ t) with

„

bool b set to true and clock z reset when φ holds.

„

When ψ holds set b to false.

≤ t

≤ t

Bounded Liveness

„ The truth value of b indicates whether or not ψ should hold in the future.

φ

ψ

¬ψ

¬φ

b=true

z=0 b=false

b true, check z ≤ t b=false

A[] (b imply z ≤ t)

E<> b (for meaningful check)

Parametric timer:

„ (re-)start(value)

start! var=value

„ expired?

active (bool) active go?

(bool+urgent chan)

„ time-out event timeout?

Declare ‘to’ with a tight range.

Timers

Zenoness

„ Problem: UPPAAL does not check for zenoness directly.

„

A model has “zeno” behavior if it can take an infinite amount of actions in finite time.

„

That is usually not a desirable behavior in practice.

„

Zeno models may wrongly conclude that some properties hold though they logically should not.

„

Rarely taken into account.

„ Solution: Add an observer automata and check for

non-zenoness, i.e., that time will always pass.

Zenoness

x ≤ 1 x ≤ 1 x=0

Zeno OK

Detect by

•adding the observer:

Constant (10) can be anything (>0), but choose it well w.r.t.

your model for efficiency.

Clocks ‘x’ are local.

•and check the property

ZenoCheck.A --> ZenoCheck.B

x ^x==1 ≥ 1