真時系統之符號式驗證程序王凡中央研究院資訊科學所

真時系統之符號式驗證程序王凡中央研究院資訊科學所
正規描述與自動驗證（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

範例：轉換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

範例（續一）：轉換 x3 x1 x1 1 1  x2 x2 x2 x2 1 1 1 1 x3 x3 x3 1 1 1 1 1

範例（續二）：轉換 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： 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) Ú z 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

如何計算  z 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 zn B(z1 ,.....,zi-1, 0, z i+1 ,.....,zn)) Ú ( zi zn B(z1 ,.....,zi-1, 1, z i+1 ,.....,zn))

假設我們有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( z 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 在q0q1q 上，每個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 修正

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

基本假設：時鐘的讀值是稠密的在兩次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 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

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

+  2. 第二步！兩兩配對，用 transitivity消去  p  y  x +5  0    2-x      15-y    3-x 與無關 在右邊 在左邊 0     15-y  15-y , 0  3-x 2-x     3-x x  15-y , 2-x  3-x 因此，得到： p  y  x +5  y15  x 3  y-x13

+  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 結束！

重要技巧：用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 兩兩配對

重要技巧：用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度空間上的投影

以不等式的所圍成的多度空間凸多面體（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三個平面所圍出來的四度空間凸多面體。

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)

給定滿足  與  的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 永遠不會發生，而系統設計正確。

真時系統之符號式驗證程序王凡中央研究院資訊科學所

Similar presentations

Presentation on theme: "真時系統之符號式驗證程序王凡中央研究院資訊科學所"— Presentation transcript:

Similar presentations

About project

反馈

请登录

Auth with social network:

真時系統之符號式驗證程序 王 凡 中央研究院 資訊科學所

Similar presentations

Presentation on theme: "真時系統之符號式驗證程序 王 凡 中央研究院 資訊科學所"— Presentation transcript:

Similar presentations

About project

反馈

真時系統之符號式驗證程序王凡中央研究院資訊科學所

Presentation on theme: "真時系統之符號式驗證程序王凡中央研究院資訊科學所"— Presentation transcript: