真時系統之符號式驗證程序 王 凡 中央研究院 資訊科學所 正規描述與自動驗證 （3） Formal Description & Automated Verification 真時系統之符號式驗證程序 王 凡 中央研究院 資訊科學所

內容 BDD與CTL模型檢驗問題 學期研究題目 並行系統的自動機組成 稠密時鐘的真時系統的模型檢驗問題 稠密時鐘的真時系統的符號式模型檢驗演算法 混和式自動機(Hybrid Automata)的符號式模型檢驗程序

二元決定圖 : BDD （Binary Decision Diagram） 邏輯公式的最小標準型（canonical form) 最小 ： 高效率 相對於特定變數評估順序 標準型 ： 同值的公式有 唯一的表示法 x 1 y z 1 1 (x Ú Øy) Ù z 1 1

BDD的函數值評估 (x Ú Øy) Ù z 以路徑traverse來評估函數值。 x 1 0 x ß ß y 0 0 y z 0 1 z 1 1 y y z z 1 1 1 1 1 1

(x Ú Øy) Ù z 變數評估順序對BDD的size影響 xßzßy xßyßz x x 1 1 z z z y y 1 z 1 1 1 1 z z z y y 1 z 1 1 1 1 1 1

BDD:邏輯函數的最小標準型 xÙ(yÚØy)Ùz x x 1 1 y 1 z z 1 1 1 1 非 BDD 正確的BDD

Even Parity 的 BDD (ØxÙØyÙØzÙØw) Ú (ØxÙØyÙzÙw) Ú (ØxÙyÙØzÙw) 1 y y (ØxÙØyÙØzÙØw) Ú (ØxÙØyÙzÙw) Ú (ØxÙyÙØzÙw) Ú (ØxÙyÙzÙØw) Ú (xÙØyÙØzÙw) Ú (xÙØyÙzÙØw) Ú (xÙyÙØzÙØw) Ú (xÙyÙzÙw) 1 1 z z 1 1 w w 1 1 1 O (n 2 n-1) O (2n+1) disjunctive normal form

BDD 的邏輯運算 Ø B1 給定兩個BDD ：B1、B2，下列邏輯函數之BDD，皆有高效率演算法，可以計算。 (Bryant 1986, IEEE Trans. Computers) B1 Ú B2 B1 Ù B2 Ø B1

由ordered的非BDD，轉換成BDD xi xi-node Reduce(G) 假設評估順序為 x1,x2,…,xn, 由0,1開始轉換， 相同的node，由其中一個取代。 然後由 i＝n 做到 1 除去所有的xi-node， 若其0-child和1-child是相同的。 0-child與1-child相同的xi-node， 由其中一個取代。 1 0-child 1-child

由ordered的非BDD，轉換成BDD 範例： 轉換0,1 x1 x1 1 1  x2 x2 x2 x2 1 1 1 1 x3 x3 x3 x3 1 1 1 1 1 1 1

由ordered的非BDD，轉換成BDD 範例（續一）： 轉換 x3 x1 x1 1 1  x2 x2 x2 x2 1 1 1 1 x3 x3 x3 1 1 1 1 1

由ordered的非BDD，轉換成BDD 範例（續二）： 轉換 x2 x1 x1 1 1  x2 x2 x2 1 1 1 x3 x3 1 1 1 1

由B1、B2，計算B1 OP B2 B10 B11 B20 B21 B10 OP B20 B11 OP B21 B1 B2 xi 1 1 B10 B11 B20 B21 B1 OP B2 xi 註：此結果需再經reduce轉化。 1 B10 OP B20 B11 OP B21

Ø(x1 x3)(x2 x3) 範例： x1 x2 x3 x3 x1 x2 x2 x3 x3 x3 + + 1 1 1 1 1 1 1 1 x3 x3 1 1 Ø(x1 x3)(x2 x3) 1 1 x1 1 x2 x2 1 1 x3 x3 x3 1 + 1 + 1 1 1 1 1

範例： x1 x2 Ø(x1 x3)(x2 x3) x3 x3 x1 x2 x3 x3 x3 + + 1 1 1 1 1 1 1 1 Ø(x1 x3)(x2 x3) 1 x3 x3 1 1 x1 1 1 1 1 x2 1 x3 x3 x3 + 1 1 1 + 1 1 1

範例： x1 x2 Ø(x1 x3)(x2 x3) x3 x3 x1 x2 x3 x3 + + 1 1 1 1 1 1 1 1 1 1 Ø(x1 x3)(x2 x3) 1 x3 x3 1 1 1 1 x1 1 1 x2 1 x3 x3 1 1 1 1 + + 1

範例： x1 x2 Ø(x1 x3)(x2 x3) x3 x3 x1 x2 x3 x3 1 1 1 1 1 1 1 1 1 1 1 1 Ø(x1 x3)(x2 x3) 1 x3 x3 1 1 1 1 x1 1 1 x2 1 x3 x3 1 1 1 1 1

範例： x1 x2 Ø(x1 x3)(x2 x3) x3 x3 x1 x2 x3 1 1 1 1 1 1 1 在reduction之後 1 x3 x3 1 1 1 1 x1 1 x2 在reduction之後 1 x3 1 1

由B，計算ØB 交換 與 1 的位置。 x1 x3 Ø(x1 x3) x1 x1 1 1 x3 x3 1 1 1 1

BDD處理的complexities Reduce(B) O(|B|log|B|) B1 OP B2 O(|B1||B2|)

Workout for BDD 1. 請畫出((Øx1) x3)  (x2  x3)的BDD。 2. 請畫出 (Ø(x1  x3)  (x2  x3))  (((Øx1) x3)  (x2  x3)) 的BDD。

用BDD達成自動驗證 系統狀態由系統二元變數值決定 n 個二元變數 2n 個狀態 x1, x2, ......, xn state(x1, x2, ......, xn)

用BDD達成自動驗證 x1 x2 x3 state(x1, x2, x3) = (x1ÙØx2Ùx3) Ú (Øx1ÙØx2Ùx3) 1 0 1 0 0 1 0 1 0 state(x1, x2, x3) = (x1ÙØx2Ùx3) Ú (Øx1ÙØx2Ùx3) Ú (Øx1Ùx2Ù Ø x3)

transition(x1, x2, ......, xn, y1, y2, ......, yn) 用BDD達成自動驗證 以二元決定圖表達系統狀態轉換的條件 2n 個變數的邏輯函數 transition(x1, x2, ......, xn, y1, y2, ......, yn) x1, x2, ......, xn y1, y2, ......, yn

用BDD達成自動驗證 x1 x2 x3 y1 y2 y3 transition(x1, x2, x3 , y1, y2, y3 ) = 1 0 1 0 0 1 0 1 0 transition(x1, x2, x3 , y1, y2, y3 ) = (x1ÙØx2Ùx3ÙØy1ÙØy2Ùy3) Ú (Øx1ÙØx2Ùx3ÙØy1Ùy2Ù Ø y3) Ú (Øx1Ùx2Ù Ø x3ÙØy1ÙØy2Ùy3 )

用BDD達成自動驗證 以BDD表達系統狀態長程路徑(path)轉換的條件 2n 個變數的邏輯函數 reach(x1, x2, ......, xn, y1, y2, ......, yn) x1, x2, ......, xn y1, y2, ......, yn

用BDD達成自動驗證 x1 x2 x3 y1 y2 y3 reach(x1, x2, x3 , y1, y2, y3 ) = 1 0 1 0 0 1 0 1 0 reach(x1, x2, x3 , y1, y2, y3 ) = (x1ÙØx2Ùx3ÙØy1ÙØy2Ùy3) Ú (x1ÙØx2Ùx3ÙØy1Ùy2ÙØy3) Ú (Øx1ÙØx2Ùx3ÙØy1Ùy2Ù Ø y3) Ú (Øx1Ùx2Ù Ø x3ÙØy1ÙØy2Ùy3 ) Ú (Øx1ÙØx2Ùx3ÙØy1ÙØy2Ùy3) Ú (Øx1Ùx2Ù Ø x3Ù Øy1Ùy2Ù Ø y3)

用BDD達成Reachability Analysis 設若 s0 為系統啟始（開機）狀態，而 sk 為危險狀態。 設若 s0 由變數值 x1, x2, ......, xn 描述， 而 sk 由變數值 y1, y2, ......, yn 描述。 Safety analysis 可以表達為計算 reach(x1, x2, ......, xn, y1, y2, ......, yn) 若reach(x1, x2, ......, xn, y1, y2, ......, yn)是『真』，則代表系統危險。 注意：『真』在BDD中只有唯一的表示法，即 1

用BDD達成CTL model-checking 定義 pathψ(x1, x2, ......, xn, y1, y2, ......, yn) ψ ψ ψ ψ ? (x1, x2, ......, xn) (y1, y2, ......, yn) 存在一個由狀態(x1, x2, ......, xn)到狀態(y1, y2, ......, yn)的路徑，且在此路徑上ψ一直被滿足，除了也許在終點。

用BDD達成CTL model-checking 給定ψ的BDD： Bψ (x1,x2 , ...... , xn)， transition的BDD：T (x1 , x2 ,....., xn,y1,y2 ,..... ,yn) 計算 pathψ(x1, x2, ......, xn, y1, y2, ......, yn)的BDD？ B0:= Bψ(x1,x2 , ...... , xn)ÙT(x1,x2 ,....., xn,y1,y2 ,.....,yn) For k:= 1 to …. Bk := Bk-1(x1,x2 ,....., xn,y1,y2 ,.....,yn) Ú z1..... zn (Bk-1(x1,x2 ,....., xn,z1,z2 ,.....,zn) Ù Bk-1(z1,z2 ,....., zn,y1,y2 ,.....,yn)) until Bk=Bk-1 Bk (x1 ,....., xn,y1,.....,yn) iff 兩個狀態間有path長度 2k

用BDD達成CTL model-checking 如何計算  z1..... zn B(z1 ,.....,zn)的BDD？ zn B(z1 ,.....,zn) = B(z1 ,.....,zn-1,0) Ú B(z1 ,.....,zn-1,1) For i := n-1 to 1, do  zi..... zn B(z1 ,.....,zn) = ( zi+1..... zn B(z1 ,.....,zi-1, 0, z i+1 ,.....,zn)) Ú ( zi+1..... zn B(z1 ,.....,zi-1, 1, z i+1 ,.....,zn))

用BDD達成CTL model-checking 假設我們有model M、與CTL公式φ φ的子公式，由小到大為φ1φ2 ...φn For i := 1 to n, do if φ= x, B(φ):=B(x) Ù state(x1, x2, ......, xn) if φ= φ1 Ú φ2 , B(φ ) :=B(φ1 ) Ú B (φ2 ) if φ= Øφ1, B (φ ) :=ØB (φ1 ) if φ= φUψ , Bφ:= B( z1..... zn pathφ (x1,......, xn, z1 ,.....,zn) Ùψ (z1 ,.....,zn)) if φ= φ , Ù pathφ (z1 ,....., zn, z1 ,.....,zn))

並行系統的自動機組成 在實際的並行(concurrent)系統中，系統往往由數個獨立描述組成。 如何建構系統的整體自動機？ 如何照顧系統的執行公平性？ 是否有個獨立的子系統，永遠輪不到執行？ 如此的計算(computatoin)，是否有意義？

並行系統的自動機組成 一個並行系統中的有限狀態自動機 A=P, Q, q0, , E,  P: 所有共用Boolean變數的集合 (P)：所有P中變數，所組成的Boolean公式的集合 Q : 控制點的集合 q0 : 啟始控制點  : Q (P)；各控制點的恆定條件 EQQ : 控制點轉換(transitions)的集合  : E (P)；各轉換的激發條件(triggering condition)

並行系統的自動機組成 狀態條件敘述（state predicate）： 以proposition集合P中的元素，建構而成 pP; 縮寫： true  p(p) 12  ((1)(2)) 1 2  (1)2 (P)：所有由P中元素建構而成的狀態條件敘述之集合

並行系統的自動機組成 Cartesian Product of A1 , A2 , ... , An , 給定 Ai=Qi, qi,0, i, Ei, i 1 i  n Cartesian Product of A1 , A2 , ... , An , A=Q, q0, , E,  Q : Q1 Q2 ...  Qn q0 : [q1,0 , q2,0 ,... , qn,0] ([q1, q2 , ... , qn])= 1(q1)  2(q2)  ...  n(qn) E([q1,...,qj1, qj , qj+1,..., qn],[q1,...,qj1, rj , qj+1,..., qn]) 根據 interleaving語意，一次只有一個 transition 發生  ([... ... , qj , ... ...],[... ... , rj , ... ...]) = i ( qj , rj )

並行系統的自動機組成 範例： p q p q p q q ＝ p  r pq q r p ( q) r pq ( q) r

並行系統的自動機組成 A,q ╞ φ iff ？ 如何照顧系統的執行公平性？ 是否有個獨立的子系統，永遠輪不到執行？ 如此的計算(computatoin)，是否有意義？ 此問題只有在無限的computation中，才造成問題。因為公平是個無限計算的觀念。 A,q ╞φUψ iff ？ A,q ╞ φ iff ？

並行系統的自動機組成 從qk開始，有一個無限的計算，每個concurrent automata都有無限多次transition 如何照顧系統的執行公平性？ A,q ╞ φUψ iff 存在一個 q0q1q2 ... qk A,qh ╞ φ, 0 h k A,qk ╞ ψ 從qk開始，有一個無限的計算，每個concurrent automata都有無限多次transition 從 qk，可以走到一個SCC(strongly connected component)。在此SCC中，每個concurrent automata都有transition。

並行系統的自動機組成 A,q ╞ φ iff 存在一個 q0q1q2 ... ... A,qh ╞ φ, 0 k 在q0q1q2 ... ...上，每個concurrent automata都有無限多次transition 從 q，可以經由維持φ條件的路徑，走到一個SCC(strongly connected component)。在此SCC中，每個concurrent automata都有transition，且每個狀態都滿足φ。

狀態空間的建立方法（一） Backward reachability analysis Use weakest precondition to compute state-spaces backward reachable from goal states The mandatory method for model-checking More like refutation Very often can lead to smaller state-space represenation Very often can lead to less total ordering enumeration

狀態空間的建立方法（二） Forward reachability analysis Use strongest postcondition to compute state-spaces forward reachable from initial states Can only be used for safety analysis Very often can lead to larger state-space represenation Very often can lead to unnecessary total ordering enumeration Need symmetry reduction and partial-order reduction

並行系統狀態空間的建立方法（一） Very often creates many unreachable states Cartesian product method Construct all the vectors of component process states Eliminate all those inconsistent vectors according to invariance condition Draw arcs from vectors to vectors according to process transitons Very often creates many unreachable states

並行系統狀態空間的建立方法（二） Starting from the initial states (or goal states in backward analysis) Step by step, add states that is reachable from those already reached, until no more new reachable states are generated. Tedious but may result in much smaller reachable state-space reprsentation.

dense-time真時自動機的模型檢驗 簡介 dense-time真時自動機的定義 語法 語意 Timed CTL (TCTL)的定義 真時自動機的模型檢驗演算法 真時自動機的符號式模型檢驗演算法

Real-Time 系統的研究 何謂Real-Time System？ 一個系統，對外界的刺激，需在指定的時間，提供正確的反應。 航空電子 戰場管制 飛彈導引 潛艇聲納分析 核能電廠監視 生命醫療監視 化學反應爐監控 航管系統

Real-Time 系統的研究 比較：傳統的非real-time系統 在有限計算時，以precondition與postcondition間的關係，定義其正確性。 在無限計算時，以事件的順序來定義其正確性。 有限狀態自動機 mutual exclusion fairness

Real-Time 系統的研究 何謂Real-Time System？ 一個系統，對外界的刺激，需在指定的時間，提供正確的反應。 範例：同步機槍 違背時間限制的善意服務，比不作還可能糟糕。

為何要dense-time clock？ 為何不用discrete clock？則可以擴充有限狀態自動機，作真時系統驗證模型。 在工程上，只要將時鐘的最小刻度定得夠細緻，就可以模擬精細的時間變化。況且，real-time系統還是用discrete clock來對事件作時間標籤。

為何要dense-time clock？（待續） 從模型的精確度上來說， 因為concurrent clocks，所以沒有辦法假設concurrent時鐘的整數值都在同時發生。若是假設整數值的變動順序，則還不如用dense-time clock算了。 因為在理論上，永遠沒有夠細緻的時鐘精密度。即時系統都控制著昂貴的設備與寶貴的資源、人命，因此不容出錯。

為何要dense-time clock？ 從複雜度上來說， 過渡細緻的時間刻度，會導致大的時間常數。而即時系統驗證問題的複雜度，與時間常數的大小成正比。 稠密變數線性系統，求solution的演算法，是在PTIME； 而整數線性系統的演算法是NP-complete。

規則系統行為: dense-time automata 即時（real-time) 系統行為 每50ms監測敵蹤並修正飛彈方向，直到命中目標為止 監控 命中 50ms 修正

規則系統行為: dense-time automata 即時（real-time) 系統行為 在500ms的限期內，每50ms監測敵蹤並修正飛彈方向，直到命中目標為止 x:=0; z:=0 監控 x<500ms z<50ms x、 z 是實數值系統時鐘。 在任何時刻，x、z以同樣數律 增加讀值 x、z在系統開始時，被設為零。 命中 z=50ms z在每次監控週期，被設為零。 z:=0; 修正

規則系統行為: dense-time automata 基本假設： 時鐘的讀值是稠密的 在兩次reset之間，時鐘的讀值是連續的。 所有時鐘以同一速率增加讀值。 因時鐘讀值是稠密的，所以狀態空間是無限的。 沒有一個next state的清晰概念。 驗證問題的基本挑戰 如何在無限的狀態空間，以有限的時間、空間來進行驗證？

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

 ::= p | x  c | xcy+d | 1 | 12 真時自動機 狀態條件敘述（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建構而成的狀態條件敘述之集合

真時自動機 A=Q, q0, , E, ,  Q : 有限控制點的集合 q0 : 啟始控制點  : Q(P,X)；各控制點的恆定條件 EQQ : 控制點轉換(transitions)的集合  : E (P, X)；各轉換的激發條件(triggering condition)  : E 2X : 在轉換時，要被reset成零（歸零）的時鐘變數的集合

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

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

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

真時自動機的語意 兩個狀態的符號定義 給定一個 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)

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

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

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

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

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

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

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

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φ

TCTL的語意 A=Q, q0, , 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 ...

TCTL的語意 A=Q, q0, , E, ,  A,(q,) ╞ φ1U cφ2 iff 存在 (q,)-run：s0 s1 s2 ... sk ... ... ... ，與 nonmonotonically increasing、divergent的非負實數序列：t0 t1 t2 ......與 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

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

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

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

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

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

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

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

TCTL模型檢驗問題 對所有  (CA:  CA:φ)， (q, )(q’,‘)，若 q = q’ 對所有 p  P，(p) = ’(p) 對所有x  X，(x) 與’(x) 在小於CA:φ時，整數部分相等 若(x)  CA:φ  ’(x)  CA:φ ，則 (x) = ’(x) 對所有x,y  X {0} ，(x) 與’(x) 在小於CA:φ時， 小數部分的順序相同。 若(x)  CA:φ’(x)  CA:φ ，則 (x) (x) (y) (y) iff ’(x) ’(x) ’(y) ’(y)

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

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

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

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

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 。

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

Workout 在給定時鐘集合X與最大時間常數CA:時，請導出Region的數目複雜度上限。

dense-time真時系統的符號式處理 p  x 3  y  x+5 s1 q  x+6  y+8 y 15 y:=0 請問在s0中， 這個transition會發生的最弱條件為何？ 經過 0 後，仍然在s0中的最若條件為何？

請問在s0中，這個transition會發生的最弱條件為何？ p  x 3  y  x+5 s1 q  x+6  y+8 y 15 y:=0 在y:=0之後， q  x+6  y+8  y=0 在y:=0之前， x+6-8  y  y  0  0  y; 兩兩配對消去 y  x+6-8  y  0  0  y  0  x-2  0 在triggering之後， x-2  0  y 15 在invariancing之後x-2  0  y 15 p  x 3  y  x+5

在s0中的狀態，經過時間前進 0 後，仍然在 x-2  0  y 15 p  x 3  y  x+5最弱條件為何？ +  1. 第一步！在s0 經過 0 的條件(s0 +  )： 0    x+ -2  0  y+15  p  x+3  y+x++5 = 0    2-x      15-y  p    3-x  y  x +5 = p  y  x +5  0    2-x      15-y    3-x 與無關 在右邊 在左邊

在s0中的狀態，經過時間前進 0 後，仍然在 x-2  0  y 15 p  x 3  y  x+5最弱條件為何？ +  2. 第二步！兩兩配對，用 transitivity消去  p  y  x +5  0    2-x      15-y    3-x 與無關 在右邊 在左邊 0     15-y 0  15-y , 0  3-x 2-x     3-x 2-x  15-y , 2-x  3-x 因此，得到： p  y  x +5  y15  x 3  y-x13

在s0中的狀態，經過時間前進 0 後，仍然在 x-2  0  y 15 p  x 3  y  x+5最弱條件為何？ +  3. 第三步！加入s0 的 invariance條件 p  y  x +5  y15  x 3  y-x13  p  x 3  y  x+5 仍然得到 p  y  x +5  y15  x 3  y-x13 結束！

dense-time真時系統的符號式處理 重要技巧： 用transitivity，兩兩配對，消去 x f1(x1, ..., xn) x  f2(x1, ..., xn) x  ... fh(x1, ..., xn) x  x g1(x1, ..., xn) x g2(x1, ..., xn)... x gk(x1, ..., xn) 存在 x 的實數解的條件是  1 i  k  1 j  k (fi (x1, ..., xn) gj(x1, ..., xn)) i、j 兩兩配對

dense-time真時系統的符號式處理 重要技巧： 用transitivity，兩兩配對，消去 x f1(x1, ..., xn) x  f2(x1, ..., xn) x  ... fh(x1, ..., xn) x  x g1(x1, ..., xn) x g2(x1, ..., xn)... x gk(x1, ..., xn) 在幾何（geometry）上的意義： x, x1, ..., xn構成的 n+1度空間的多面體 在x1, ..., xn 構成的n度空間上的投影

dense-time真時系統的符號式處理 以不等式的所圍成的多度空間凸多面體（convex hull），來代表等價的狀態集合。 x 3  y  x+5  z  x+5 是由x=3  y = x+5  z = x+5三個平面所圍出來的三度空間凸多面體。 x 3  y  x+5  z  w +5 是由x=3  y = x+5  z = w+5三個平面所圍出來的四度空間凸多面體。

dense-time真時系統的符號式處理 p  x 3  y  x+5 s1 q  x+6  y+8 y 15 y:=0 請問在s0中， 這個transition會發生的最弱條件為何？ 經由前述推導過程，我們可以製作程序：xtion_bck(s,e) 經過 0 後，仍然在s0中的最若條件為何？ 經由前述推導過程，我們可以製作程序：time_bck(s)

dense-time真時系統的符號式處理 給定滿足  與  的symbolic 表示法， 要如何評估   U< c  ？ S:=   <c ; S’:=false; while S  S’ { S’:= S; S:= S  (  e  T time_bck ( xtion_bck (S, e) ) } return   ( =0  S) ; /* 用transitivity兩兩配對消去 法，除掉  ＊/

Workout for symbolic verification of timed automata 給定一個transition (q,q’): when x  11 may y:= 0; 與invariance條件 (q): 4  y  y < 25 與狀態空間條件：  = 9 < x  x-y  7  y  5 請計算 xtion_bck ( , (q, q’) ) 請計算 time_bck ( xtion_bck ( , (q,q’) ) )

混合式自動機(hybrid automata) 自動機 + 連續變數 連續變數 ：有理數、或實數。 如溫度、水量、速度、距離等。 以連續變數值、及其一次變率之不等式表達合格的系統狀態 溫度 > 100℃ Ù 水量 < 400l 以連續變數值、及其一次變率之不等式表達合格的系統狀態轉換 溫度增加率 = 6℃/秒 Ù水量 < 400l

混合式自動機(hybrid automata) 一個鍋爐控制系統。有水含量、溫度、水流量。 100℃溫度 109℃ 溫度 109℃ Ù水量400l 水量2000l 水量2000l Ù 進水率=400l/秒

混合式自動機的驗證理論 線性 ： 容許之即時條件需為如 6x + y + 5 < 2z + 12 之線性基本條件之有限Boolean組合。 reachability problem並無解法 (not decidable) 在線性即時 (real-time) 系統下 x+5 < y model-checking問題有演算法可解

混合式系統驗證問題之符號式處理 Cornell 的 Henzinger 的HyTech 系統狀態由系統連續變數值決定 x1, x2, ......, xn 溫度 > 100℃ Ù 水量 < 400l

混合式系統驗證問題之符號式處理 以連續變數值、及其一次變率之不等式表達合格的系統狀態 以連續變數值、及其一次變率之不等式表達合格的系統狀態轉換 以連續變數值、及其一次變率之不等式表達合格的系統長程狀態轉換 可就給定之系統啟始狀態 s0 與危險狀態 sk 計算此不等式。 若此不等式條件是邏輯『假』值，則 sk 永遠不會發生，而系統設計正確。