Computer Aided Verification 計算機輔助驗證 Model Checking (Part II) 模型檢驗 (二)

Presentation on theme: "Computer Aided Verification 計算機輔助驗證 Model Checking (Part II) 模型檢驗 (二)"— Presentation transcript:

1 Computer Aided Verification 計算機輔助驗證 Model Checking (Part II) 模型檢驗 (二)
CTL, TCTL, and Symbolic Model Checking) (Chapters: 4, 17, 5, 6 of “Model Checking” book) Pao-Ann Hsiung Department of Computer Science and Information Engineering National Chung Cheng University, Taiwan 熊博安 國立中正大學 資訊工程研究所 These slide contents are adapted from the slides of Professor Farn Wang.

2 Contents CTL Model Checking Timed Automata (TA)
Timed Computation Tree Logic (TCTL) TCTL Model Checking Clock Zones, DBM, BDD Symbolic Model Checking Counterexample & Witnesses

3 模型檢驗（Model Checking） 模型檢驗問題的定義： 給定一個有限狀態結構 M 與一個時態邏輯公式φ，請問M是φ的一個模型嗎？

4 模型檢驗（Model Checking） 狀態空間分析 規則系統行為 有限但極大(天文數字)之狀態空間 狀態空間表示法：有向圖
節點：系統狀態 箭頭：狀態轉換 規則系統行為 有限但極大(天文數字)之狀態空間 執行 完成 等待

5 CTL模型檢驗的演算法 給定M 與φ 1. 將Closure(φ)中的公式，由小到大排列 φ0 φ1 φ2 … φn
對所有0 i<j  n，φj 不是φi 的子公式！ 2. 依序由i=0 到 n，對所有M 中的狀態 s，計算 M, s┝φi (第七頁的方法) 3. 如果M的啟始狀態是 s0，且M, s0┝φ， 則回答“是”;否則回答“否”!

6 Closure(φ) 是所有φ的子公式所成的集合
φ 的子公式為φ φψ 、 φψ 的子公式為φ 、ψ φψ的子公式為φ 、ψ φUψ的子公式為φ 、ψ 、  φUψ φUψ的子公式為φ 、ψ 、 φUψ φ、 φ 的子公式為φ φ 的子公式為φ 、 φ φ 的子公式為φ 、 φ φ的子公式為φ 、  φ φ的子公式為φ 、  φ

7 CTL模型檢驗的演算法（續） 若φi 為 true，則 M,s┝φi 若φi 為 φ，則 M,s┝φi iff not M,s┝φ
若φi 為φψ，則 M,s┝φi iff M,s┝φ 或M,s┝ψ 若φi 為 φUψ，則由所有滿足ψ 的狀態開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φUψ 若φi 為 φ，找出 M 中所有狀態都滿足φ的Strongly Connected Components（SCC）。由這些SCC開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φ。 注意： φUψ  (( φ U (φψ)) ψ)

8 CTL模型檢驗的演算法（續） 若φi為φUψ，則由所有滿足ψ 的狀態開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φUψ。
For all state s with M,s┝ψ, M,s┝ φUψ holds Repeat until no more change can be made: For all (s', s), if M,s'┝φ and M,s┝ φUψ, then M,s'┝ φUψ 此一計算一定會停止，因為每一個φUψ都是被有限長度路徑所滿足。Repeat迴圈只需循環到最長的最短路徑長度。

9 CheckEU(f1, f2) for  f1U f2

10 CTL模型檢驗的演算法（續） 若φi 為 φ，找出 M 中所有狀態都滿足φ的Strongly Connected Components（SCC）。由這些SCC開始，沿著滿足φ的所有的反向路徑上的狀態，都滿足φ。 將M中，不滿足φ的狀態都刪掉。 執行transitive closure以計算剩餘狀態間的路徑。 Reach[s,s’]=1如果由s到s’之間，有一條路徑 Reach[s,s’]=0如果由s到s’之間，沒有路徑 For all s, M,s┝ φ iff s’(Reach[s,s’]  Reach[s’,s’])

11 CTL模型檢驗的演算法（續） 在M（剩餘的M）中，所有狀態都滿足φ。 執行 transitive closure:
For all s, s do if (s, s)M, Reach[s, s] := 1; else Reach[s, s] := 0; For s, s do For all s do Reach[s, s] := Reach[s, s]  (Reach[s, s]  Reach[s, s]);

12 Strongly Connected Components (SCC)
A strongly connected component (SCC) C is a maximal sub-graph such that every node in C is reachable from every other node in C along a directed path entirely contained within C. s1 s2 s3 s4 s5 Two SCC: {s1, s2, s3} {s4}

13 CheckEG( f1) for  f1

14 Microwave Oven Example

15 Microwave Oven Example
(Start  ◇Heat) ◇(Start  Heat) S(Start) = {2, 5, 6, 7} S(Heat) = {1, 2, 3, 5, 6} SCC(Heat) = {1, 2, 3, 5} S(Heat) = {1, 2, 3, 5} S(Start  Heat) = {2, 5} S(◇(Start  Heat)) = {1,2,3,4,5,6,7} S(◇(Start  Heat)) = 

16 Fairness Constraints F = {P1, …, Pk} // fairness constraints
Fair SCC C  Pi  F, state ti  (C  Pi). CheckFairEG(f1): Fair SCCs Define “fair”: atomic proposition, true at a state s iff there is a fair path starting at s. M, s┝ p  fair, M, s┝ (f1  fair), CheckEUFair(f1, f2) = CheckEU(f1, f2fair) = M, s┝  (f1 U (f2  fair))

17 Microwave Oven (with Fairness)
(Start  ◇Heat) F = {◇(Start  Close  Error)} S(Start) = {2, 5, 6, 7} S(Heat) = {1, 2, 3, 5, 6} SCC(Heat) = {1, 2, 3, 5} is NOT fair S(Heat) = { } S(◇(Start  Heat)) = { } S(◇(Start  Heat))={1,2,3,4,5,6,7}

18 Model Checking Real-Time Systems
Timed Automata (TA) Real-Time Properties: Timed Computation Tree Logic (TCTL) Given a real-time system S modeled by a set of TA {A1, A2, …, An} and a real-time property specified by a TCTL formula , check if S satisfies  (S┝  ?).

19  ::= p | x  c | x-y  y | 1 | 12
Timed Automata真時自動機 狀態條件敘述（state predicate）： 以proposition集合P與時鐘變數集合X，建構而成  ::= p | x  c | x-y  y | 1 | 12 pP; x, y X; c,dN; ‘’{ ,  , ,  , } 範例： 男性  未婚  年齡  30 孤單  男性  未婚  今日+2  收假日 戰機巡航模式  x+5  回報週期

20  ::= p | x  c | xcy+d | 1 | 12
Timed Automata真時自動機 狀態條件敘述（state predicate）： 以proposition集合P與時鐘變數集合X，建構而成  ::= p | x  c | xcy+d | 1 | 12 pP; x, y X; c,dN; ‘’{ ,  , ,  , } 縮寫： true  x = x 12  ((1)(2)) 1 2  (1)2 (P, X)： 所有由P、X建構而成的狀態條件敘述之集合

21 Timed Automata真時自動機 A = Q, q0, P, X, , E, , 
Q : 有限控制點的集合 (set of control locations) q0 : 啟始控制點 (initial location) P : 命題的集合 (set of propositions) X : 時鐘變數的集合 (set of clock variables)  : Q (P,X)；各控制點的恆定條件 (invariant) EQQ : 控制點轉換的集合 (set of transitions)  : E (P, X)；各轉換的激發條件 (triggering condition)  : E 2X : 在轉換時，要被reset成零（歸零）的時鐘變數的集合 (set of clocks to be reset)

22 A=Q, q0, P, X, , E, ,  Q={監控，命中} E={(監控,監控),(監控,命中)}
q0=監控  (監控 ,監控)= z =50 P = { }, X = {x, y}  (監控 ,命中)= true  (監控)= x  500z  50  (監控 ,監控)= {z}  (命中)= true  (監控 ,命中)= {} 監控 x  500ms z  50ms x:=0; z:=0 命中 z=50ms z:=0

23 Parallel Composition of TA
A1=Q1, q01, P1, X1, 1, E1, 1, 1, A2=Q2, q02, P2, X2, 2, E2, 2, 2 A1 ∥A2 =  Q1  Q2, q0, P1  P2 X1  X2 , E, 1  2, 1  2  q0: a merge of q01 and q02 (q, q') = 1(q)  2(q') E: set of interleaved transitions with synchronization transitions identified

24 A Manufacturing Example

25 Manufacturing Ex: D-Robot TA

26 Manufacturing Ex: G-Robot TA

27 Manufacturing Ex: Station TA

28 Manufacturing Ex: Box TA

29 Model of Manufacturing System
M = D-Robot || G-Robot || Station || Box Transitions with same labels are identified as one in M. E.g.: g-put in G-Robot, Station, and Box E.g.: d-pick in D-Robot, Station, and Box

30 真時自動機的語意 A = Q, q0, P, X, , E, ,  狀態 s = (q,) q  Q
 : P  {true, false}  X R+ ; 定義所有Boolean變數的真假值 定義所有時鐘變數的非負實數讀值 ┝ (q) ; 時鐘讀值與proposition設定，須滿足控制點的恆定條件

31 真時自動機的語意 A=Q, q0, P, X, , E, , 
 ┝ ： 滿足一個狀態條件敘述 　　(state predicate)   ┝ p iff  (p) = true  ┝ x  c iff  (x)  c  ┝ x - y  d iff  (x) - v(y)  d  ┝ 1 iff not  ┝ 1  ┝ 12 iff ┝ 1 或 ┝ 2 狀態 s = (q,) ； s ┝  iff  ┝ 

32 真時自動機的語意 兩個狀態的符號定義 給定一個 R+，    是一個新函數 (  )(p) =  (p)
(  )(x) =  (x)   給定一個 Y X ， Y是一個新函數 (Y)(p) =  (p) (Y)(x) = 0 iff x Y (Y)(x) =  (x) iff x Y 給定 s = (q,) 與 Y  X ， sY = (q,Y)

33 真時自動機的語意 從直觀上看， dense-time自動機的計算（computation），應該是
對映到R+ （非負實數集合）的一個狀態序列； 具有狀態的稠密性；

34 真時自動機的語意 A=Q, q0, P, X, , E, ,  一個轉換 (transition) 的符號定義
給定s = (q,) 與 s' = (q', ') ， ss'（狀態 s與狀態 s'間，有一個轉換）iff (q, q')  E s┝  (q, q') s (q, q')┝  (q')

35 真時自動機的語意 A=Q, q0, P, X, , E, ,  的計算 (computation) s0-run: s0 s1 s2 ... sk 對所有k  0， sk 是具有如(q,)格式的狀態。 存在一個monotonically increasing、divergent的非負實數序列 t0 t1 t2 ... tk 對所有k  0， 對所有 t[0, tk+1tk ]， sk t┝ (q) Either sk  (tk+1tk ) = sk+1 or sk  (tk+1tk )  sk+1

36 Timed Computation Tree Logic (TCTL)
範例：從現在的狀態開始，有一種可能將來，七天會發薪水。 7發薪水 範例：從現在開始，無論將來如何，十年內要結婚。  10 結婚

37 TCTL（續） 範例：在任何計算狀態，敵機出現，都可能在五秒內擊落。 (發現敵機   5 擊落敵機))
範例： 在任何狀態，不管如何計算，敵機都會在五秒內擊落。 (發現敵機   5 擊落敵機))

38 TCTL（續） 範例：從任何狀態開始，都有一種計算，時間會無限增加。 1true
範例：從任何狀態開始，對所有計算，時間都會無限增加。 1true

39 φ ::=  | φ1 | φ1φ2 | φ1U cφ2 |  cφ1
TCTL的語法 φ ::=  | φ1 | φ1φ2 | φ1U cφ2 |  cφ1   (P, X)：所有由P、X建構而成的狀態條件敘述之集合; c  N; ‘’  {, , , , }

40 TCTL的語法 縮寫： φ1φ2  ((φ1)(φ2)) φ1 φ2  (φ1)φ2
φ1φ2  ((φ1)(φ2)) φ1 φ2  (φ1)φ2  cφ   trueU cφ  cφ    c φ φ1U cφ2  ( ((φ2)U c(φ1φ2))   cφ2)  cφ   trueU cφ

41 TCTL的語意 A=Q, q0, P, X, , E, ,  A,(q,)┝φ; 狀態 (q,) 滿足φ
A,(q,)┝ ； 定義如state predicate 者 A,(q,)┝ φ1 iff not A,(q,)┝φ1 A,(q,)┝ φ1φ2 iff A,(q,)┝φ1 或 A,(q,)┝φ2 A,(q,)┝ φ1U cφ2 iff ... A,(q,)┝  cφ1 iff ...

42 TCTL的語意 A=Q, q0, P, X, , E, ,  A,(q,)┝ φ1U cφ2 iff 存在
(q,)-run：s0 s1 s2 ... sk ，與 monotonically increasing、divergent的非負實數序列：t0 t1 t 與 k  0，與 t [0, tk+1  tk]， tk+t t0  c A,sk+t┝φ2 對所有k  h  0與 t’ [0,th+1  th]， A, sh+t’┝φ1 對所有 t’ [0 ,t)，A, sk+t’┝φ1

43 TCTL的語意 A = Q, q0, P, X, , E, ,  A,(q,)┝  cφ1 iff 存在
(q,)-run：s0 s1 s2 ... sk ，與 monotonically increasing、divergent的非負實數序列：t0 t1 t 對所有k  0，與 t [0, tk+1  tk]， 若 tk+t t0  c，則 A,sk+t┝φ1

44 A ┝φ iff  ， 若┝(q0)，則A,(q0, ) ┝φ
TCTL模型檢驗問題 定義： A ┝φ（A滿足φ ；A是φ的一個模型） 給定一個A=Q, q0, , E, , 與一個TCTL公式φ， A ┝φ iff  ， 若┝(q0)，則A,(q0, ) ┝φ TCTL模型檢驗問題： 請問A是φ的一個模型嗎？

45 TCTL模型檢驗問題的反思 如何在無限、稠密的狀態空間中，分割出有限的discrete狀態空間？ 工程經驗：
在任何即時系統中，雖然面對無限的大自然環境，在電腦的觀測中，還是以有限的flag、switch來描述，並控制系統的行為。

46 TCTL模型檢驗問題的反思 平交道監視器的範例 x:=0; x=300 x=100 x:=0; 在即時系統中，用clock來控制! 遙遠
1/2 公里內 x=300 x=100 x:=0; 火車剛剛通過 在平交道上 在即時系統中，用clock來控制!

47 TCTL模型檢驗問題的反思 Real-time systems 的自動驗證，真的是必要的嗎？ 還是只是學術上的假象？ 目前的一個困境：
在即時系統的製作上，工業界的工程師並不把系統看做real-time automata 最傳統的作法，還是periodic model 在真時工業案例中，也缺乏強有力的理由，非用real-time automata不可。

48 TCTL模型檢驗問題 如何將無限的狀態空間， 切割為有限、且等價行為的狀態子空間？

49 TCTL模型檢驗問題 符號定義： 假設在A與φ中，使用最大的常數是CA:φ 。

50 TCTL模型檢驗問題 Infinite States  Finite Regions q = q'
Two states are in the same region, i.e., (q, )  (q', ')，若 q = q' 對所有 p  P，(p) = '(p) 對所有x  X，(x) 與'(x) 在小於CA:φ時， 整數部分相等。 若  (x)  C  '(x)  C ，則 (x) = '(x) 對所有x, y  X， (x) 與 '(x) 小於CA:φ時，小數部分的順序相同。 若  (x)  C   '(x)  C ，則 (x)  (x)  (y) (y) iff '(x) '(x)  '(y) '(y)

51 TCTL模型檢驗問題 當CA:φ=7 且有兩個clock: x、y

52 2 Clocks with cx= 2, cy= 1 28 Clock Regions: 6 corner points,
14 open line segments, 8 open regions

53 TCTL模型檢驗問題 Equivalent States: (q, )  (q', ')，若 小數部分的順序相同。 q = q'
立於相同的控制點。 對所有 p  P，(p) = '(p) 可以判斷所有 Boolean 變數的真假值。 對所有x  X，(x) 與'(x) 在小於CA:φ時，整數部分相等 可以判斷所有 x  c不等式的真假值。 對所有x, y  X，(x) 與'(x) 在小於CA:φ時， 小數部分的順序相同。 可以判斷哪一個不等式 x  c會先發生變化。

54 TCTL模型檢驗問題 定理：對所有 ，若(q, )  (q', ')，則
A, (q, ) ┝  iff A, (q', ') ┝  直觀證明：若存在 (q, ) 則可以由(q', ')建立： (q',  ') 等價片段 等價片段 等價片段 等價片段 等價片段 等價片段 等價片段

55 TCTL模型檢驗問題 Region graph 以 s  s' 的等價關係，將狀態空間分割成有限數目的子空間。
[s]、 [s']之間的transition， 可以代表自動機上的狀態轉換， 也可以代表時間的前進。

56 TCTL模型檢驗問題 可以證明，以region graph就可以充分必要的回答TCTL的模型檢驗問題。
但須加上一個附加的clock變數 z， A,(q,)┝ φ1U cφ2 iff A,(q, [z])┝ φ1U cφ2  [z]與 完全一樣，除了 [z](z)= 0 A,(q, [z])┝ φ1U cφ2 iff存在由(q, [z])開始的region序列 r0 r1 r2 ... rk r0 r1 r2 ... rk-1 都滿足φ1 rk 滿足φ2 與 z  c 。

57 TCTL的驗證問題複雜度 TCTL與真時自動機的模型檢驗問題是PSPACE-complete。
TCTL的satisfiability問題，是undecidable。

58 Clock Zones Finite representation of infinite state-space
Conjunction of inequalities such as: x < c | x ≤ c | x – y < c | x – y ≤ c x, y  X, c  Z General form of a clock zone: x0 = 0  0  i  j  n (xi – xj ~ cij) ~  {< , ≤}

59 Clock Zones (Operations)
Clock zones are closed under 3 operations: Let z1, z2 be two clock zones, Y  X, t  0 Intersection: z1  z2 is a clock zone (Conjunction of conjunctions) Clock Reset: z1(Y:=0) is a clock zone (Proof on pages 284 ~ 287) Time Elapse: z1 + t is a clock zone (See next page)

60 Clock Zones (Time Elapse)

61 Zones = Symbolic States
Zone: (s, z), where s: location, z: clock zone represents a symbolic state. Successor Clock Zone: z' = succ(z, e), where z: clock zone, e: transition (successor clock zone obtained from z after time elapse and executing transition e) Successor Zone: (s', succ(z, e)), where e: ss'

62 Clock Zone (succ(z, e)) To obtain Successor Clock Zone (succ(z, e))
Intersect z with  (s) Let time elapse in s (operator te()) Intersect with  (s) Intersect with  (e) Reset all clocks from  (e) succ(z, e) = ((te(z (s))  (s)   (e))[ :=0]) Closed under , te(), reset, also a clock zone!!!

63 a transition: (s, z)  (s', succ(z, e))
Zone Graph Zone Graph is a transition system Z(A) States = zones of A Initial state = (s, [X := 0]) For each transition e of A: a transition: (s, z)  (s', succ(z, e)) Zone reachability State reachability

64 Difference Bound Matrix (DBM)
DBM is a matrix to represent a clock zone 0 – x1 < c, i.e., x1 > c x1 <  x1 – xn  r xn  d

65 DBM (Example) x1  x2 < 2  0 < x2  2  1  x1

66 DBM (Uniqueness) A zone is not uniquely represented by a DBM
Zone: x1  x2 < 2  0 < x2  2  1  x1 x1  x2 < 2 and x2   x1 < 4

67 xixj ~ij dij and xjxk ~jk djk  xixk ~ik dik
DBM (Canonical Form) Canonical (unique) form of DBM for a zone Tightening operation: xixj ~ij dij and xjxk ~jk djk  xixk ~ik dik where dik = dij + djk ~ik =  if both ~ij and ~jk are  < otherwise Apply tightening operations to a DBM until no more change is possible!

68 DBM (Emptiness) Check if all elements on main diagonal are ( 0)
Yes  nonempty No  empty or unsatisfiable Empty or unsatisfiable  At least 1 negative entry on main diagonal E.g. xi  xi  1  0  1  FALSE!!!

69 DBM (3 operations: Intersection)
Intersection: D = D1  D (all DBMs) Let D1(i, j) = ~1 c1 and D2(i, j) = ~2 c2 D(i, j) = (min(c1, c2), ~) where ~ = ~1 if c1 < c2 ~ = ~2 if c2 < c1 ~ = ~1 if c1 = c2 and ~1 = ~2 ~ = < if c1 = c2 and ~1  ~2

70 DBM (3 operations: Clock Reset)
Clock Reset: D' = D [Y := 0], Y  X defined as follows: D'(i, j) = ( 0) if xi, xj  Y D'(i, j) = D(0, j) if xi  Y and xj  Y D'(i, j) = D(i, 0) if xj  Y and xi  Y D'(i, j) = D(i, j) if xj  Y and xi  Y

71 DBM (3 operations: Time Elapse)
Time Elapse: D' = te(D) defined as follows: D'(i, 0) = (< ), for any i  0 D'(i, j) = D(i, j), for i = 0 or j  0

72 DBM (3 operations) All 3 operations can be efficiently implemented
DBM must be canonalized (using tightening) before any of the 3 operations (intersection, clock reset, and time elapse) After any of the 3 operations, a DBM might no longer be canonical! Last step: Reduce to canonical form!!!

73 DBM (Zone Graph Construction)
Clock zones: represented by DBM Succesor clock zones succ(z, e): computed by the 3 operations: intersection, reset, and time elapse on DBM instead of on clock zones

74 DBM (Zone Graph Construction)
Initial state: (s0, Z0), Z0: x = 0  y = 0 Zone D0

75 DBM (Zone Graph Construction)
Invariant  (s0) is 0 ≤ x  0 ≤ y ≤ 5

76 DBM (Zone Graph Construction)
Step 1: Intersection D0 with  (s0) gives D0 Step 2: Let time elapse: te(D0   (s0) )

77 DBM (Zone Graph Construction)
Step 3: Intersect with  (s0) again

78 DBM (Zone Graph Construction)
Trigger (a) = y  3

79 DBM (Zone Graph Construction)
Step 4: Intersect with trigger (a)

80 DBM (Zone Graph Construction)
Step 5: Reset clock y in DBM Z1 = 3 ≤ x ≤ 5  3 ≤ x  y ≤ 5  y = 0

81 DBM (Zone Graph Construction)
Successor of (s0, Z0) is (s1, Z1) Repeat the same 5 steps: (s0, 4 ≤ y ≤ 5  4 ≤ y  x ≤ 5  x = 0) (s1, 0 ≤ x ≤ 1  0 ≤ x  y ≤ 1  y = 0) (s0, 5 ≤ y ≤ 8  5 ≤ y  x ≤ 8  x = 0) (s1, x = 0  y = 0), which is contained in the 2nd zone, thus no more new zones can be generated!!! No more change! Stop! Zone Graph!

82 Binary Decision Diagram (BDD)
BDD: A canonical form representation for Boolean formulas. Motivation: Too much space redundancy in traditional representations BDD is more compact than truth tables, conjunctive normal form, disjunctive normal form, binary decision trees, etc. BDD has a canonical form BDD operations are efficient

83 BDD (Binary Decision Tree)

84 BDD (redundancy in BDT)
Binary Decision Trees (BDT): Same size as truth tables Lots of redundancy: Out of 8 subtrees rooted at b2 only 3 are distinct!!! Merge isomorphic subtrees  BDD BDD is a rooted, DAG with 2 types of vertices: terminal and nonterminal Each nonterminal v is labeled with var(v) and has two successors: low(v) and high(v) Each terminal vertex is labeled 0 or 1

85 BDD (Boolean Function)
BDD B with root v determines Boolean function fv(x1, …, xn) as follows: If v is a terminal vertex fv(x1, …, xn) = value(v)  {0, 1} If v is a nonterminal vertex with var(v) = xi: fv(x1, …, xn) = ( xi  flow(v)(x1, …, xn) )  ( xi  fhigh(v)(x1, …, xn))

86 BDD (Canonical Form) Canonical Form:
Two boolean functions are logically equivalent iff they have isomorphic representations Why Canonical Form? Simplifies equivalence checking and satisfiability checking BDD Canonical Form: Same variable order along all paths from root to terminal No isomorphic subtrees or redundant vertices

87 BDD (Canonical Form) For requirement 1 (same variable order):
Total ordering < on all variables If u has a nonterminal successor v, then var(u) < var(v) For requirement 2 (no redundancy): Apply 3 transformations repeatedly: Remove duplicate terminals Remove duplicate non-terminals Remove redundant tests

88 BDD (Canonical Form) Remove duplicate terminals: Eliminate all but one terminal vertex with a given label and redirect hanging arcs. Remove duplicate non-terminals: If var(u) = var(v), low(u) = low(v), high(u) = high(v), then eliminate u or v. Redirect hanging arcs. Remove redundant tests: If low(v) = high(v), then eliminate v and redirect incoming arcs to low(v).

89 BDD (Canonical Form) Apply 3 transformations repeatedly in a bottom-up manner Time: O(|BDD|) Gives Ordered BDD (OBDD) Order: a1 < b1 < a2 < b2 OBDD for two-bit comparator example

90 Ordered BDD (OBDD) Since OBDDs are canonical, it is easy to:
check equivalence = check BDD isomorphism check satisfiability = check BDD isomorphism with OBDD(0) Size of OBDD depends critically on VARIABLE ORDERING!!! 2-bit comparator example: Change variable order to: a1 < a2 < b1 < b2 11 vertices instead of 8 for a1 < b1 < a2 < b2

91 OBDD (Variable Ordering)
a1 < a2 < b1 < b2 In general, for n-bit comparator: a1 < b1 < …< an < bn gives 3n + 2 vertices a1 < …< an < b1<…< bn gives 3  2n  1 vertices

92 OBDD (Variable Ordering)
Infeasible to find an optimal variable ordering! Checking a particular ordering is optimal is NP-complete! There are Boolean functions with exponential size OBBDs for any ordering! Eg: nth output of a combinational circuit to multiply two n bit integers

93 OBDD (Variable Ordering)
Heuristics to find a good variable ordering: Depth-First Traversal of circuit gives a good variable order Intuition: related variables should be grouped together in the order Dynamic Reordering: to save time and space, not to find an optimal ordering.

94 f = ( x  f |x:=0)  (x  f |x:=1)
OBDD (Operations) All 16 two-argument logical operations can be implemented efficiently on OBDDs. Time Complexity = O(|OBDD1|  |OBDD2|) Key Idea: Shannon Expansion f = ( x  f |x:=0)  (x  f |x:=1) Let f, f ' = OBDDs, v, v' = roots, x = var(v), x' = var(v') Apply(f, f ', *, ): a uniform algorithm for all 16 operations *

95 OBDD (Apply Algorithm)
If v, v' are terminals, f * f ' = value(v) * value(v') If x = x', then use Shannon Expansion: f * f ' = ( x  (f |x:=0 * f '|x:=0))  ( x  f |x:=1 * f '|x:=1)) If x < x', then Shannon Expansion simplifies: f * f ' = ( x  (f |x:=0* f '))  (x  f |x:=1 * f ')) (∵ f '|x:=0 = f '|x:=1 = f ' does not depend on x) If x' < x, same as previous.

96 OBDD (Efficiency) A problem generates 2 sub-problems
Use dynamic programming to avoid exponential algorithm # sub-graphs = |OBDD(f )| A sub-problem depends on 2 sub-graphs # sub-problems ≤ |OBDD(f1)|  |OBDD(f2)| Result Cache: computed sub-problems in canonical form Modern BDD package: millions of vertices!

97 OBDD (Representing Kripke Structures)
State variables: a, b Add new state variables: a', b' s1s2: (a  b  a'  b') Full system: (a  b  a'  b')  (a  b  a'  b')  (a  b  a'  b')

98 Symbolic Model Checking
Symbolic = Manipulation of Boolean formulas Symbolic  Operate on entire sets of states instead of individual states and transitions

99 Fixpoint Representations
M(S, R, L): Finite Kripke Structure P(S): power set of S Least element in P(S): False = empty set Greatest element in P(S): True = S Predicate transformer:  : P(S)  P(S) 0(Z) = Z,  i+1(Z) =  i(Z)  is monotonic if P  Q   (P)   (Q)

100 Fixpoint Representations
Fixpoint characterization of temporal logic operators A set S'  S is a fixpoint of a function  : P(S)  P(S) if  (S') = S'. (S: set of states, P(S): power set of S) A monotonic predicate transformer  on P(S) always has: a least fixpoint:  Z. (Z) a greatest fixpoint:  Z. (Z)

101 Least Fixpoint False   (False)   2(False)  …
No. of iterations  |S| Last iteration:  (Q) = Q =  Z. (Z)  Z. (Z)  (False) False

102 Least Fixpoint Algorithm

103 Greatest Fixpoint True   (True)   2(True)  …
No. of iterations  |S| Last iteration:  (Q) = Q =  Z. (Z) True = S  (True) 2 (True)  Z. (Z)

104 Greatest Fixpoint Algorithm

105 Fixpoint Characterizations
 =  Z .  Z  =  Z .   Z  =  Z .   Z  =  Z .   Z [1 U 2] =  Z . 2  (1  Z) [1 U 2] =  Z . 2  (1  Z)    Z   Z

106 Approximations for [p U q]

107 Symbolic Model Checking for CTL
Kripke Structures are represented symbolically using OBDDs. Quantified Boolean Formulas QBF(V): every propositional variable in V is a formula f, f  g, f  g are formulas, if f and g are v f and v f are formulas, if f is and vV Every QBF formula can be represented by an OBDD x f = f |x=0  f |x= x f = f |x=0  f |x=1

108 Symbolic Model Checking Algorithm
Check(a CTL formula) returns an OBDD that represents all system states satisfying the formula Inductive definition of Check() as follows: If f = a (a proposition), Check(f ) returns the set of states satisfying a. If f = f1 f2 or f = f1, use Apply(Check(f1), Check(f2), *)

109 Symbolic Model Checking Algorithm
Check(f ) = CheckEX(Check(f )) Check([f U g]) = CheckEU(Check(f ), Check(g)) Check(f ) = CheckEG(Check(f )) CTL formula OBDD

110 CheckEX(f ) f is true in a state if it has a successor in which f is true. CheckEX(f (v)) = v'[f (v')  R(v, v')] = [f (v')  R(v, v')]|v'=0  [f (v')  R(v, v')]|v'=1 R is the transition relation OBDD Given OBDDs for f and R, we can compute an OBDD for v'[f (v')  R(v, v')]

111 CheckEU(f ) Least fixpoint characterization: [1 U 2] =  Z . 2  (1  Z) Use Lfp() to compute Q0=False, Q1, …, Qi, … that converges to [1 U 2] Given OBDDs for 1, 2, and Qi, we can compute Qi+1. Qi+1= 2  (1  Qi) Qi+1= Qi  Qi=  Z . 2  (1  Z)

112 CheckEG(f ) Greatest fixpoint characterization  =  Z .   Z
Use Gfp() to compute Q0=True, Q1, …, Qi, … that converges to  Given OBDDs for 1 and Qi, we can compute Qi+1. Qi+1 =    Qi Qi+1= Qi  Qi=  Z .   Z

113 Fairness in Symbolic Model Checking
Fairness Constraints F = {P1, …, Pn}  =  Z .   k = 1…n[ U(Z  Pk)] Set of all states which are start of some fair computation is fair(v) = CheckFair(True) CheckFairEX(f (v)) = CheckEX(f (v)  fair(v)) CheckFairEU(f(v), g(v)) = CheckEU(f(v), g(v)  fair(v))

114 Counterexamples & Witnesses
Counterexample: If  is false, produce a path to a state in which  holds. Witness: If  is true, produce a path to a state in which  holds. Counterexample() = Witness( ) Thus, need consider only witnesses: , U, and .

115 Witnesses Construct SCC graph G(V, E), where each node in V is an SCC, and an edge exists if there is a transition from a state in one SCC to a state in another SCC. SCC graph contains no cycle (because all cycles are in SCC graph nodes) Each infinite path has a suffix in an SCC graph node.

116 Witness for  with F = {P1,…,Pk}
 =  Z .   k = 1…n[ U(Z  Pk)] For each P, compute an increasing sequence of approximations Q0P  Q1P  Q2P  …, where QiP is the set of states from which a state in Z  P can be reached in  i steps. Start with an initial state s satisfying  . Look for a successor t of s in Q0P, PF. If no such t, keep looking in Q1P, Q2P, … If t  QiP and i > 0, find a successor of t in Qi-1P, and continue until i = 0, thus we have a path from s to some state u in   P. Continue with other PF to obtain s'. Find a path from s' to t (cycle).

117 Witness for  in first SCC

118 Witness for  spans 3 SCC

119 Witnesses for U and  fair = {s | state s satisfies True with F}
Witness for  [ f U g] with F = Witness for  [ f U (g  fair)] Witness for [ f ] with F = Witness for [ f  fair]

120 An ALU Example

121 An ALU Example Pipeline circuit
First cycle of instruction: read operands from register file into operand registers Second cycle: compute result and store in first pipe register Third to r + 1 cycle: result is passed through remaining pipeline registers Last cycle: result is written to register file

122 An ALU Example Only after r + 2 cycles, the result of an operation is written back to register file. Input signal stall  invalid instruction (e.g., cache miss)  no change to destination reg Assume: 1 pipe register, XOR op only CTL specification has 2 parts: Destination register updated correctly All other registers should not change

123 Spec Part 1 (Dest reg updated correctly)
An ALU Example Spec Part 1 (Dest reg updated correctly) Use n operator for n cycle delays src1opi = (src1addr  2 reg0,i)  (src1addr  2 reg1,i) src2opi = (src2addr  2 reg0,i)  (src2addr  2 reg1,i) resulti = (destaddr  3 reg0,i)  (destaddr  3 reg1,i)

124 Spec Part 2 (No change in other registers)
An ALU Example Spec Part 2 (No change in other registers) ((stall  destaddr)  (2reg0,i 3reg0,i)) ((stall  destaddr)  (2reg1,i 3reg1,i))

125 An ALU Example (Experiment Results)
8-bit wide pipeline 4 general registers 1 pipeline register 1 operation More than 1020 states 41,000 OBDD nodes Verification time: 22 mins of Sun 3 Substantial improvement over explicit-state model checking