Introduction to SAT Based Abstraction Refinement in Model Checking

1. Introduction to Formal Methods for SW and HW Development 09: SAT Based Abstraction/Refinement in Model-Checking Roberto Sebastiani Based on work and slides by E. Clarke, A. Gupta , J. Kukula, O. Strichman (CAV02) revisions by M. Roveri, R. Sebastiani and S. Tonetta

2. 2 Outline Preliminaries Notion of Abstraction Over and under-approximation, simulation, bisimulation Counter-example based abstraction refinement

3. 3 Model Checking Given a: Finite transition system M ( S , I , R , L ) A temporal property p The model checking problem: Does M satisfy p ?

4. 4 Model Checking Temporal properties: Always when a train arrives the bar is not up G (train_arriving !bar_up ) Every Send is followed immediately by Ack G (Send X Ack) Reset can always be reached GF Reset From some point on, always switch_on FG switch_on Safety properties Liveness properties

5. 5 Model Checking (safety) I Add reachable states until reaching a fixed-point = bad state

6. 6 Model Checking (safety) I PROBLEM: Too many states to handle ! = bad state

7. 7 Abstraction h h h h h Abstraction Function h : S ! S S S

8. 8 Abstraction Function Partition variables into visible( V ) and invisible( I ) variables. The abstract model consists of V variables. I variables are made inputs. The abstraction function maps each state to its projection over V .

9. 9 Abstraction Function 0 0 0 0 0 0 0 1 0 0 1 0 0 0 1 1 x 1 x 2 x 3 x 4 0 0 h x 1 x 2 Group concrete states with identical visible part to a single abstract state.

10. 10 Building an Abstract Model M can be computed efficiently if M is in functional form, e.g. sequential circuits. Abstract x 1 x 2 x 3 x 4 x 1 x 2 i 1 i 2 i 1 i 2 x 3 x 4

11. 11 Building an Abstract Model (cont.) next(x1) = f1(x1,x2,x3,x4,i1,i2); next(x2) = f2(x1,x2,x3,x4,i1,i2); next(x3) = f3(x1,x2,x3,x4,i1,i2); next(x4) = f4(x1,x2,x3,x4,i1,i2); next(x1) = f1(x1,x2,x3,x4,i1,i2); next(x2) = f2(x1,x2,x3,x4,i1,i2); abstract

12. 12 Computing Abstractions S concrete state space S abstract state space : S S - abstraction : S 2 S : (s) = {s | s=h(s)} - concretization (refinement) Properties of and : ( (A)) = A, for A in S ( (B)) B, for B in S The above properties mean that and are Galois-connected S S

13. 13 Aside: simulations M = (s 0 , S, R, L) M = (t 0 , S, R, L) Definition: p is a simulation between M and M if 1. (s 0 , t 0 ) p 2. (t, t 1 ) R (s, s 1 ) R s.t. (s, t) p and (s 1 , t 1 ) p (We say that M simulates M.) Intuitively, for every transition in M there is a corresponding transition in M

14. 14 Aside: bisimulation M = (s 0 , S, R, L) M = (t 0 , S, R, L) Definition: p is a bisimulation between M and M if 1. p is a simulation between M and M and 2. p is a simulation between M and M

15. 15 Existential Abstraction (Over- Approximation): M simulates M I I

16. 16 Model Checking Abstract Model Preservation Theorem M M Intuition: if M has a countermodel,M simulates it The counterexample may be spurious The c onverse does not hold M M Let be a universally-quantified property (i.e., expressed in LTL or ACTL) and M simulates M

17. 17 Universal Abstraction (Under- Approximation): M simulates M I I

18. 18 Model Checking Abstract Model Preservation Theorem M M Intuition: if M has a model, M simulates it Converse does not hold M M Let be a existential-quantified property (i.e., expressed in ECTL) and M simulates M

19. 19 Model Checking Abstract Model M = (s 0 , S, R, L) and M = (t 0 , S, R, L) related by bisimulation Then, for every CTL/LTL property : M M M M

20. 20 Our specific problem Preservation Theorem M M Converse does not hold M M Counter-examples may be spurious Let be a universally-quantified property (i.e., expressed in LTL or ACTL) and M simulates M

21. 21 Checking the Counterexample Counterexample : (c 1 , ,c m ) Each c i is an assignment to V . Simulate the counterexample on the concrete model.

22. 22 Checking the Counterexample Concrete traces corresponding to the counterexample (c1, ,cm): (Initial State) (Unrolled Transition Relation) (Restriction of V to Counterexample)

23. 23 Abstraction-Refinement Loop Check Counterexample Refine Model Check Abstract M, p M, p, h No Bug Pass Fail Bug Real Spurious h

24. 24 Refinement methods P Frontier Inputs Invisible Visible (R. Kurshan, 80s) Localization

25. 25 Generate all counterexamples. Prioritize variables according to their consistency in the counterexamples. X1 x2 x3 x4 ( Glusman et al. , 2002) Intels refinement heuristic Refinement methods

26. 26 Simulate counterexample on concrete model with SAT If the instance is unsatisfiable, analyze conflict Make visible one of the variables in the clauses that lead to the conflict ( Chauhan, Clarke, Kukula, Sapra, Veith, Wang, FMCAD 2002) Abstraction/refinement with conflict analysis Refinement methods

27. 27 Why spurious counterexample? I I Deadend states Bad States Failure State f

28. 28 Refinement Problem: Deadend and Bad States are in the same abstract state. Solution: Refine abstraction function. The sets of Deadend and Bad states should be separated into different abstract states. D to represent the set of Deadend states B to represent the set of Bad states

29. 29 Refinement h h h h h Refinement : h h h

30. 30 Refinement Deadend States Let f be the maximum value by which the following formula is satisfiable:

31. 31 Refinement Deadend States Bad States

32. 32 Refinement as Separation The state separation problem Input: Sets D , B o f states (assignments) Output: U (minimal) subset of I s.t.: d D, b B, u U . d(u) b(u) The refinement h is obtained by adding U to V .

33. 33 Refinement as Separation 0 1 0 1 0 1 0 0 0 1 0 0 1 0 0 1 1 1 0 1 0 d 1 b 1 b 2 I V 0 1 1 1 0 1 Refinement : Find subset U of I that separates between all pairs of deadend and bad states. Make them visible. Keep U small !

34. 34 Refinement as Separation 0 1 0 1 0 1 0 0 0 1 0 0 1 0 0 1 1 1 0 1 0 d 1 b 1 b 2 0 1 1 I V Refinement : Find subset U of I that separates between all pairs of deadend and bad states. Make them visible. Keep U small !

35. 35 Two separation methods ILP-based separation Minimal separating set. Computationally expensive. Decision Tree Learning based separation. Not optimal. Polynomial.

36. 36 Separation with Decision Tree learning (Example) Separating Set : {v 1 ,v 2 ,v 4 } D B B D B D 1 0 0 1 b 1 d 2 d 1 b 2 v 1 v 4 v 2 0 1 { d 1 , b 2 } { d 2 , b 1 } D B Classification:

37. 37 Separation with 0-1 ILP One constraint per pair of states. v i = 1 iff v i is in the separating set.

38. 38 Separation with 0-1 ILP (Example)

39. 39 Refinement as Learning For systems of realistic size Not possible to generate D and B . Expensive to separate D and B . Solution: Sample D and B Infer separating variables from the samples. The method is still complete: counterexample will eventually be eliminated.

40. 40 Efficient Sampling D B d b Let (D,B) be the smallest separating set of D and B . Q : Can we find it without deriving D and B ? A : Search for smallest d , b such that (d,b) = (D,B)

41. 41 Efficient Sampling Direct search towards samples that contain more information. How? Find samples not separated by the current separating set (Sep).

42. 42 Efficient Sampling Recall: D characterizes the deadend states B characterizes the bad states D B is unsatisfiable Samples that agree on the sep variables: Rename all v i B to v i

43. 43 Efficient Sampling Sep = {} d , b = {} Run SAT solver on ( Sep ) STOP unsat Compute Sep:= (d,b) Add samples to d and b sat Sep is the minimal separating set of D and B

44. 44 The Tool NuSMV Cadence SMV MC Chaff SAT LpSolve Dec Tree Sep

45. 45 Results Property 1

46. 46 Results Property 2 Efficient Sampling together with Decision Tree Learning performs best. Machine Learning techniques are useful in computing good refinements.

47. 47 Current trends (3/3) ( Chauhan, Clarke, Kukula, Sapra, Veith, Wang, FMCAD 2002) Abstraction/refinement with conflict analysis

48. 48 The End