Presentation

3-Valued Abstraction-Refinement
Sharon Shoham
Academic College of Tel-Aviv Yaffo
1
Model Checking
An efficient procedure that receives:
 A finite-state model describing a system
 A temporal logic formula describing a property
It returns
yes, if the system has the property
no + Counterexample, otherwise
[EC81,QS82]
•3
Model Checking

Emerging as an industrial standard tool for
verification of hardware designs: Intel,
IBM, Cadence, …

Recently applied successfully also for
software verification: SLAM (Microsoft),
Java PathFinder and SPIN (NASA), BLAST
(EPFL), CBMC (Oxford),…
•4
Model of a System
Kripke structure / transition system
a,b
a
a
b,c
b
a,c
Labeled by atomic
propositions AP
(critical section,
variable value…)
a,b
c
Notation: M = (AP, S, s0, R, L)
States Initial Transitions Labeling
state
SxS
S 2Lit
5
Temporal Logics
Express properties of event orderings in time
• Linear Time
– Every moment has a
unique successor
– Infinite sequences
(words)
– Linear Time Temporal
Logic (LTL)
• Branching Time
– Every moment has several
successors
– Infinite tree
– Computation Tree Logic
(CTL), CTL*, -calculus
6
Propositional Temporal Logic
AP – a set of atomic propositions
Temporal operators:
Xp
Gp
Fp
pUq
Path quantifiers: A for all paths
E there exists a path
7
LTL / CTL / CTL*
LTL – of the form A
 - path formula, contains no path quantifiers
• interpreted over infinite computation paths
CTL – path quantifiers and temporal operators appear
in pairs: AG, AU, AF, AX, EG, EU, EF, EX
• interpreted over infinite computation trees
CTL* - Allows any combination of temporal operators
and path quantifiers. Includes both LTL and CTL
8
ACTL / ACTL*
The universal fragments of the logics, with
only universal path quantifiers
– Negation is allowed only on atomic propositions
9
Main Limitation of Model Checking
The state explosion problem:
Model checking is efficient w.r.t. to the state
space of the model. But…
The number of states in the system model grows
exponentially with
 the number of variables
 the number of components in the system
10
“Solutions” to the State Explosion Problem
Symbolic model checking:
The model is represented symbolically
• BDD-based model checking
• SAT-based Bounded/ Unbounded model checking
Small models replace the full, concrete model:
•
•
•
•
Abstraction
Compositional verification
Partial order reduction
Symmetry
11
Outline
• Background:
– Model Checking
– Abstraction
– CEX guided abstraction-refinement (CEGAR)
• 3-Valued Abstraction Refinement (TVAR)
• Example: TVAR for CTL
• Investigation of abstract models used in TVAR
–
–
–
–
Monotonicity of Refinement
Completeness
Precision
Efficiency
12
Abstraction-Refinement
• Abstraction: removes or simplifies details
that are irrelevant to the property under
consideration
Can reduce the number of states
– from large to small
– from infinite to finite
• Refinement might be needed
13
Widely used Abstractions

Localization reduction / invisible variables: each
variable either keeps its concrete behavior or is
fully abstracted (has free behavior) [Kurshan94]


Initially: unabstracted variables are those appearing in the
checked property
Predicate abstraction: concrete states are
grouped together according to the set of
predicates they satisfy [GS97,SS99]

Initially: predicates are extracted from the program’s
control flow and the checked property
15
Abstraction Example
(x  y)
xy
Abstract states
Concrete states
x=0 x=1
y=2 y=2
x=2
y=2
x=3
y=2
x=4
y=2
…
16
Abstraction Example
(x  y)
xy
• Abstraction (SA, ):

– Finite set of
abstract states SA
– Abstraction mapping
 : SA →2Sc
not necessarily disjoint sets
x=0 x=1
y=2 y=2
x=2
y=2

x=3
y=2
x=4
y=2
…
17
Abstraction Example
(x  y)
xy
• Abstraction (SA, ):

– Finite set of
abstract states SA
– Abstraction mapping
 : SA →2Sc
not necessarily disjoint sets
x=0 x=1
y=2 y=2
x=2
y=2

x=3
y=2
x=4
y=2
…
• Concrete Kripke structure MC = (SC, RC, LC)
Abstract model over SA: labeling, transitions
Need to be conservative
18
Why Conservative?
Goal:
• Model check MA instead of MC
• Deduce result over MC from result over MA
What can we deduce?
• true ?
• false ?
• Both ?
For which properties?
Depends on abstract model and abstract semantics
19
2-valued CounterExample-Guided
Abstraction Refinement (CEGAR)
For ACTL*
[CGJLV00, JACM2003]
•20
Abstraction preserving ACTL/ACTL*
Existential Abstraction:
every concrete transition is represented by an abstract
transition
If sc(sa) s’c(s’a) s.t.
(sc, s’c)RC then (sa,s’a)RA
Formally: simulation
sa
sc
s’a


s’c
The abstract model is an over-approximation of the
concrete model:
– The abstract model has more behaviors
– no concrete behavior is lost
•21
Simulation Relation
H  SC x SA is a simulation relation from
MC to MA if whenever (sc, sa)  H:
• LC(sc)  LA(sa)
• If (sc, sc’)  RC for some sc’, then there
exists sa’ s.t. (sa,sa’)  RA and (sc’, sa’)  H
If there exists a simulation relation obeying
the initial states, then MC sim MA
•22
Existential Abstraction
• Abstract model is also a Kripke structure
• Same semantics is used for abstract and
concrete models
 Same model checking algorithms
Abstract model checking result is true or false
(2-valued)
But… what can we deduce?
•23
Logic Preservation Theorem
Theorem. Let MC sim MA. Then:
• Every ACTL/ACTL* property true in the
abstract model is also true in the concrete
model:
MA |=   MC |= 
However, the reverse may not be valid:

If MA | , need to check further

Check if abstract counterexample is spurious
•24
CEX Guided Abstraction Refinement
M and  ACTL/ACTL*
generate initial
abstraction
MA
MA
|= 
model check
MA |= 
Refinement:
based on cex
TA
is spurious
generate
counterexample TA
TA
check spurious
counterexample
stop
TA is not spurious
•25
Three-Valued Abstraction Refinement
(TVAR)
for Full CTL*
[SG03,GLLS05]
•26
2-valued Approach is not Applicable
• Over-approximation (simulation) of the
concrete model is not sound for
verification of existential properties:
MA |= E does not imply MC |= E
 More complex abstract models (and
relations) are needed to ensure logic
preservation
•27
Abstract Models for CTL*
Branching-time temporal logics combining
existential (E) and universal (A) quantifiers:
 two transition relations [LT88]
– Rmay: an over-approximation
– Rmust: an under-approximation
Rmay used to verify A … and falsify E
Rmust used to verify E … and falsify A
•28
Logic Preservation for CTL*
If MA is an abstraction of MC then for every
CTL* formula ,
MA |=   MC |= 
MA |   MC | 
• But sometimes [MA |=  ] = don’t know
 3-Valued Semantics
3 possible values: True, False ,  (indefinite)
•29
Refinement
• Refinement is needed when result is 
Traditional abstraction-refinement for universal
properties not applicable:
–
–
Refinement needed when result is false
Based on a counterexample
Three-Valued Abstraction-Refinement
(TVAR)
•30
The TVAR Methodology
M and  CTL/CTL*
generate initial
abstraction
MA
Refinement:
Based on failure
model check
[MA |=3 ] = tt,ff
[MA |= 3 ] = 
find and analyze
failure cause
stop
•31
Main Components
1. Abstract Models:
What formalism is suitable?
How to construct an abstract model in a
conservative way?
2. Model Checking:
How to evaluate branching-time formulas over
abstract models based on the 3-valued semantics?
3. Refinement:
How to refine the abstract model?
•33
TVAR for CTL using
Kripke Modal Transition Systems
[SG03]
•34
Abstract Models
Kripke Modal Transition System (KMTS)
[HJS01]
• M = (AP, S, s0, Rmust, Rmay, L)
– Rmust  S x S: an under-approximation
– Rmay  S x S: an over-approximation
– Rmust  Rmay
For simplicity.
In MixTS, no such requirement
•35
Abstract Models
Labeling function :
• L: S→ 2Literals
• Literals = AP ⋃ {p | pAP }
• At most one of p and p is in L(s).
– Concrete: exactly one of p and p is in L(s).
– KMTS: possibly none of them is in L(s),
meaning that the value of p in s is unknown
•36
3-Valued Semantics
[BG99]
lit (s) = tt if litLA(s), ff if litLA(s),  o.w.

tt if forall s’, if (s, s’) Rmay,
then  (s’) = tt
AX (s) = ff if exists s’ s.t. (s, s’)Rmust
“all succ. satisfy ”
and  (s’) = ff
 otherwise
EX (s) - dual
“exists succ. satisfying ”
•37
Construction of Abstract Model
Labeling of abstract states
¬p
MA
p

MC
¬p
¬p
¬p

p
¬p

p
[sc(sa) litLC(sc) ]
p
p
 litLA(sa)
•38
Construction of Abstract Model
must and may transitions:
must: under
approximation
()
MA
MC



[sc(sa) sc’(sa’) s.t. (sc,sc’)RC]  (sa,sa’)Rmust
Construction of Abstract Model
must and may transitions:
may: over
approximation
()
MA
MC



[sc(sa) sc’(sa’) s.t. (sc,sc’)RC]  (sa,sa’)Rmay
Mixed Simulation
H  SC x SA is a mixed simulation relation from
Kripke structure MC to KMTS MA if whenever
(sc, sa)  H:
• LC(sc)  LA(sa)
• If (sc, sc’)  RC, then there is sa’ s.t. (sa,sa’)  Rmay
and (sc’, sa’)  H
• If (sa, sa’)  Rmust, then there is sc’ s.t. (sc, sc’)  RC
and (sc’, sa’)  H
If there exists a mixed simulation relation
obeying the initial states, then MC mix MA
•41
Logic Preservation
Theorem.
Let MC mix MA. Then:
For every CTL* formula ,
MA |=   MC |= 
MA |   MC | 
But if [MA |= ] = , the value in MC is unknown
•42
3-Valued Model
Checking Example
M:
s p, q
p, q t
 = AXp EXq
•43
3-Valued Model
Checking Example
(s, AXpEXq)
state of
the model
M:
s p, q
p, q t
 = AXp EXq
formula that
we want to
evaluate in s0
MC graph
•44
3-Valued Model
Checking Example
(s, p)
Terminal
(t, p)
s p, q
p, q t
 = AXp EXq
(s, AXpEXq)
(s, AXp)
M:
(s, EXq)
(s, q)
Terminal Terminal
(t, q)
Terminal
MC graph
•45
tt
ff
Coloring the graph
⊥
s p, q
p, q t
 = AXp EXq
(s, AXpEXq)
(s, AXp)
M:
(s, EXq)
Model’s transitions
(s, p)
(t, p)
(s, q)
(t, q)
need to consider:
• may vs. must
Terminal nodes: based on states labeling
,, AX, EX: according to sons, based on semantics
•46
3-Valued Model Checking Results
• tt and ff are definite: hold in the
concrete model as well.
• ⊥ is indefinite
⇒ Refinement is needed.
•47
Refinement
• done by splitting abstract states
(as for the case of 2-values)
•MA
•MC
•
•
•
•48
Refinement
• Uses the colored MC graph
• Find a failure node nf:
– a node colored  whereas none of its sons was
colored  at the time it got colored.
– the point where certainty was lost
• purpose: change the  color of nf .
•49
Example
tt
ff
M:
s p, q
⊥
p, q t
 = AXp EXq
(s, AXpEXq)
failure
(s, AXp)
(s, p)
(t, p)
(s, EXq)
(s, q)
(t, q)
reason for failure:
may-son
- not enough to verify
- prevents refutation
•50
Failure Reason
• Failure reason is either:
– A may-edge which is not a must-edge.
– A ⊥-terminal node
• Back in the model:
– Either a transition (s, s’)  Rmay\Rmust:
 Split s to get a must-transition or none.
•53
Failure Reason
• Failure reason is either:
– A may-edge which is not a must-edge.
– A ⊥-terminal node
• Back in the model:
– Either a transition (s, s’)  Rmay\Rmust:
 Split s to get a must-transition or none.
•54
Failure Reason
• Failure reason is either:
– A may-edge which is not a must-edge.
– A ⊥-terminal node
• Back in the model:
– Either a transition (s, s’)  Rmay\Rmust:
 Split s to get a must-transition or none.
– Or (s,lit) where lit ∉ L(s), ¬lit ∉ L(s)
 Split s according to lit.
•55
Failure Reason
• Failure reason is either:
p
¬p
– A may-edge which is not a must-edge.
– A ⊥-terminal node
• Back in the model:
– Either a transition (s, s’)  Rmay\Rmust:
 Split s to get a must-transition or none.
– Or (s,lit) where lit ∉ L(s), ¬lit ∉ L(s)
 Split s according to lit.
•56
Split
• Refinement is reduced to separating sets
of concrete states.
– done by known techniques [CGJLV00,CGKS02]
 Refined abstraction mapping.
• Build refined abstract model and refined
MC-graph accordingly.
•57
Example (cont.)
(s2, p)
(t, p)
s1 p,p,qq
p,p, qq tt
 =p,AXp
q EXq
s2
(s1, AXpEXq)
(s1, AXp)
M:
M’:
 = AXp EXq
(s1, EXq)
(s2, q)
(t, q)
•59
tt
ff
Example (cont.)
⊥
(s2, p)
(t, p)
s1 p, q
p, q t
s2 p, q
(s1, AXpEXq)
(s1, AXp)
M’:
 = AXp EXq
(s1, EXq)
(s2, q)
(t, q)
•60
Incremental Abstraction-Refinement
No reason to split states for which MC
results are definite during refinement.
• After each iteration remember the nodes
colored by definite colors.
• Prune the refined MC graph in sub-nodes of
remembered nodes.
[ (sa, ) is a sub-node of (sa’, ’) if =’ and (sa)⊆’(sa’) ]
• Color such nodes by their previous colors.
•61
Example
•62
Example (cont.)
Refined MC-graph
•63
Example (cont.)
•64
Example (cont.)
Refined MC-graph
…
•65
Are KMTSs good enough for TVAR?
67
Investigation of Abstract Models
•
•
•
•
Monotonicity of Refinement
Precision
Completeness
Efficiency
68
(1) Monotonicity of Refinement
Is a refined abstract model at least as
precise as the unrefined one?
69
Example
P ::
input x > 0
pc=1: if x>5 then x := x+1 else x := x+2
pc=2: while true do
if odd(x) then x := -1 else x := x+1
 = EF (x ≤ 0)
70
An Abstract Model M
pc=1
s0
x>0
P ::
input x > 0
pc=1: if x>5 then x := x+1
else x := x+2
pc=2: while true do
if odd(x) then x := -1
else x := x+1
s2
s1
pc=2
x>0
pc=2
x0
[ EF (x ≤ 0) ] (M) =

71
s0
s1
pc=1
The abstract model M
x>0
s2
pc=2
x>0
pc=2
x0
s00
pc=1 x>0
odd(x)
A refinement
s10
M’ of M
pc=2
x>0
odd(x)
P ::
input x > 0
pc=1: if x>5 then x := x+1
else x := x+2
pc=2: while true do
if odd(x) then x := -1
else x := x+1
pc=1 x>0
odd(x)
s11
pc=2 x>0
odd(x)
s01
s20
pc=2 x0
odd(x)
s21
pc=2 x0
odd(x)
72
pc=1
s0
The abstract model M
x>0
s1
[ EX (x > 0) ] (M) =
s2
pc=2
x>0
pc=2
x0
s00
pc=1 x>0
odd(x)
A refinement
s10
M’ of M
pc=2
x>0
odd(x)
M’ CTL M
[ EX (x > 0) ] (M’) =
tt
P ::
input x > 0
pc=1: if x>5 then x := x+1
else x := x+2
pc=2: while true do
if odd(x) then x := -1
else x := x+1
pc=1 x>0
odd(x)
s11
pc=2 x>0
odd(x)
s01
s20
pc=2 x0
odd(x)
s21
pc=2 x0
odd(x)

73

Problem
• When splitting states during refinement
we may lose must transitions
• Existential formulas that were true before
may become indefinite !
(also universal formulas that were false)
• Thus, the refined model is not necessarily
more precise
 refinement is not monotonic
74
Goal: define a refinement that adds underapproximated must transitions
[current refinements remove over-approximated may
transitions ]
Result: refined model will be more precise,
i.e. more formulas will be definite (tt or ff)
in it:
Monotonic Refinement
Notation: M’ CTL M : M’ is more precise than M
75
Refinement M’’ of M, according to Godefroid et. al.
s0
s1
pc=1
s00
x>0
s2
pc=2
x>0
pc=2
x0
pc=1 x>0
odd(x)
s10
pc=2 x>0
odd(x)
pc=1 x>0
odd(x)
s01
s11
pc=2 x>0
odd(x)
s20
pc=2 x0
odd(x)
s21
pc=2 x0
odd(x)
M’’ CTL M
76
(2) Precision
Given a state abstraction (SA, )
• “How many” formulas can be verified or
falsified on the abstract model?
77
Refinement M’’ of M, according to Godefroid et. al.
s0
s1
pc=1
s00
x>0
s2
pc=2
x>0
pc=2
x0
pc=1 x>0
odd(x)
pc=1 x>0
odd(x)
s10
pc=2 x>0
odd(x)
s01
s11
pc=2 x>0
odd(x)
s20
pc=2 x0
odd(x)
s21
pc=2 x0
odd(x)
M’’ CTL M
[ EF (x ≤ 0) ] (M’’)=

78
Another Solution
[SG’04]
Use hyper-transitions as must transitions
Hyper-transition from a state s  S is
• (s, A) where and A  S is nonempty
79
Generalized KMTS (GTS)
M = ( S, S0, Rmay, Rmust, L)
• S, S0, Rmay, L as before
• Rmust  S x 2S
80
Constructing an Abstract GTS
Given MC, SA, and  : SA →2Sc
• (sa, A)  Rmust only if -condition holds:
sc (sa) s’aA s’c(s’a) :
(sc, s’c)  Rc
sa
sc
must

A

s’c
every state in (sa) has a corresponding transition
81
Reminder: in KMTS:
Constructing
anonly
Abstract
GTS holds:
(sa, s’a)  Rmust
if -condition
sc (sa) s’c(s’a) : (sc, s’c)  Rc
Given MC, SA, and  : SA →2Sc
• (sa, A)  Rmust only if -condition holds:
sc (sa) s’aA s’c(s’a) :
(sc, s’c)  Rc
sa
sc
must

A

s’c
every state in (sa) has a corresponding transition
82
3-Valued Semantics over GTS
lit (s) = tt if litLA(s), ff if litLA(s),  o.w.

tt if forall s’, if (s, s’) Rmay,
then  (s’) = tt
AX (s) = ff if exists A  SA s.t. (s, A)Rmust
“all succ. satisfy ”
and  (s’) = ff forall s’A
 otherwise
EX (s) - dual
“exists succ. satisfying ”
84
Must Hyper-transition ()
s00
pc=1: if x>5 then x := x+1
else x := x+2
Pc=2: …
pc=1 x>0
odd(x)
s10
pc=2 x>0
odd(x)
s11
pc=2 x>0
odd(x)
Every concrete state in (s00) has a transition
to a concrete state in either (s10) or (s11)
85
Generalized KMTS MG
s00
pc=1 x>0
odd(x)
s01
pc=1 x>0
odd(x)
P ::
input x > 0
pc=1: if x>5 then x := x+1
else x := x+2
pc=2: while true do
if odd(x) then x := -1
else x := x+1
s20
s11
s10
pc=2 x>0
odd(x)
pc=2 x>0
odd(x)
MG ≤CTL M’’ ≤CTL M and
pc=2 x0
odd(x)
s21
pc=2 x0
odd(x)
[ EF (x ≤ 0) ] (MG) = tt
86
Monotonicity Theorem:
Let MA and M’A be two abstract GTSs of Mc
such that
• M’A is obtained from MA by splitting states
• Both MA and M’A are exact
Then M’A is more precise than MA
87
M and 
generate initial
abstraction
MA
refinement
model check
tt, ff

find and analyze
failure state
stop
To complete the picture…
• Extension of the game-based 3-Valued
Model Checking and Failure Analysis to
GTSs
88
Investigation of Abstract Models
•
•
•
•
Monotonicity of Refinement
Precision
Completeness
Efficiency
89
(3) Completeness
• Suppose MC |= 
• Does there exist a finite abstraction (SA,)
such that [MA |= ] = tt?
90
Monotonicity vs. Completeness vs.
Precision
• Monotonicity of refinement:
Given two abstractions, where one is a split of the
other, is refined abstraction more precise than
unrefined one?
• Precision:
How many formulas can be verified on the abstract
model, with a given abstraction (SA, ) ?
• Completeness:
Does there exist an abstraction (SA, ) for which we
can verify the formula on the abstract model?
91
Are KMTSs complete?
• No fairness constraints
incomplete for liveness properties
What about Safety? (no least fixpoint)
No [Dams & Namjoshi, 2004]
But GTSs are! [de Alfaro et al, 2004]
92
Investigation of Abstract Models
•
•
•
•
Monotonicity of Refinement
Precision
Completeness
Efficiency
93
(4) Efficiency
Cost:
- Size of the abstract model w.r.t. |SA|
- Efficiency of Model Checking
94
Drawback of GTS
The number of must hyper transitions might be
exponential in the number of abstract states |SA|
Optimization:
including only (s, A) such that A is minimal
• Does not change precision of the abstract model
But, might still be too large
95
In Practice
• Not all hyper-transitions are relevant for
specific model checking problem
s0
EXp(s0) = ?
“exists a successor
that satisfies p”
p
…
p
…
…
p
 Need to find designated hyper-transitions
96
Alternative Approach [SG06]
• Compute hyper-transitions during Model
Checking, by need
 Game-based Model Checking
97
Our Algorithm
Ordinary
transitions
• Compute over approximation of concrete
transition relation
(sa, s’a)RA iff
sc(sa) s’c(s’a) : (sc, s’c)  Rc
All reachable states are considered
• Construct MC graph based on RA
• Apply bottom up coloring
98
During Coloring
s ⊢ EX
s1⊢ s2⊢ s3⊢ s4⊢ s3⊢ s3⊢
tt
tt
ff
tt
ff
ff
…
sn⊢
tt
Att: all states in which the value of  is tt
(s, Att) meets -condition [must]? yes: EX(s0) = tt
99
During Coloring
s ⊢ EX
s1⊢ s2⊢ s3⊢ s4⊢ s3⊢ s3⊢
tt
tt
ff
tt
ff
ff
…
sn⊢
tt
Aff: all states in which the value of  is ff
(s, Att) meets -condition [must]? yes: EX(s0) = tt
All may transitions reach Aff ?
otherwise: EX(s0) = 
yes: EX(s0) = ff
100
Abstract Model Checking
• Loops: slight complication
In the paper [SG06]:
Comparable to
the complexity
without hypertransitions
• Abstract MC for the alternation-free -calculus
• Complexity: O(|SA|2 x ||)
• In particular: num of  checks,
num of hyper transitions
As precise as constructing the full GTS
101
Abstraction-Refinement
• If (s0) = , apply refinement by
splitting abstract states, as in [SG03]
• Refinement is monotonic:
refined model is more precise, i.e. more calculus formulas are definite (tt or ff) in it
 Abstraction-refinement loop
102
Summary
We presented the TVAR framework for
3-valued abstraction-refinement in model
checking:
• Properties preserved:
– CEGAR: truth of ACTL*
– TVAR: both truth and falsity of Full CTL*
• Refinement eliminates
– CEGAR: Counterexamples
– TVAR: indefinite results ()
103
Summary
The TVAR framework requires
1. Different abstract models (Rmust, Rmay)
– Rmust is harder to compute, and problematic
in terms of monotonicity, precision,
completeness, and efficiency
– KMTS, GTS, HTS
2. Adapted Model checking for new models:
– 3-valued Coloring of MC-graph
104
Summary
The TVAR framework requires
3. Refinement eliminating indefinite results
– Identify failure state and cause
– Incremental abstraction-refinement (similar
to lazy abstraction in 2-valued MC)
Gives benefits in preciseness and in the
properties preserved
105