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) xy 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) xy • 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) xy • 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 | pAP } • 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 litLA(s), ff if litLA(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) litLC(sc) ] p p litLA(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, AXpEXq) 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, AXpEXq) (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, AXpEXq) (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, AXpEXq) 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, AXpEXq) (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, AXpEXq) (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 x0 [ EF (x ≤ 0) ] (M) = 71 s0 s1 pc=1 The abstract model M x>0 s2 pc=2 x>0 pc=2 x0 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 x0 odd(x) s21 pc=2 x0 odd(x) 72 pc=1 s0 The abstract model M x>0 s1 [ EX (x > 0) ] (M) = s2 pc=2 x>0 pc=2 x0 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 x0 odd(x) s21 pc=2 x0 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 x0 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 x0 odd(x) s21 pc=2 x0 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 x0 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 x0 odd(x) s21 pc=2 x0 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’aA 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’aA 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 litLA(s), ff if litLA(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 x0 odd(x) s21 pc=2 x0 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