第8講模型檢測

1、u白盒測試和黑盒測試白盒測試和黑盒測試u靜態(tài)測試靜態(tài)測試和動態(tài)測試（和動態(tài)測試（驗證測試和確認測試驗證測試和確認測試）u傳統(tǒng)測試方法和面向?qū)ο鬁y試的方法傳統(tǒng)測試方法和面向?qū)ο鬁y試的方法直接檢查源代碼或其它文檔l同行評審同行評審l桌面檢查桌面檢查l代碼審查代碼審查l走查走查l軟件驗證軟件驗證l也稱好友評審也稱好友評審l不是很正式：不是很正式：“你把你的拿給我看看，我把你把你的拿給我看看，我把我的拿給你看看我的拿給你看看”l由軟件設(shè)計和編碼人員加上一兩個其它程序由軟件設(shè)計和編碼人員加上一兩個其它程序員或測試人員組成員或測試人員組成l對源程序代碼進行人工分析、檢驗對源程序代碼進行人工分析、檢驗l關(guān)注

2、變量值和程序邏輯關(guān)注變量值和程序邏輯l記錄檢查結(jié)果記錄檢查結(jié)果l最好由非程序作者本人模擬執(zhí)行程序最好由非程序作者本人模擬執(zhí)行程序l只有一個人在閱讀代碼，沒有團隊協(xié)作只有一個人在閱讀代碼，沒有團隊協(xié)作5示例示例l軟件業(yè)最佳實踐軟件業(yè)最佳實踐l重點放在查找工作產(chǎn)品缺陷上重點放在查找工作產(chǎn)品缺陷上l文檔必須通過質(zhì)量關(guān)卡（文檔必須通過質(zhì)量關(guān)卡（核對表，核對表，ChecklistChecklist）n角色l主持人：主持人：控制進度，分派和跟蹤任務，報告審查結(jié)果控制進度，分派和跟蹤任務，報告審查結(jié)果l作者：作者：陳述項目的概況，解釋代碼中不清晰的部分陳述項目的概況，解釋代碼中不清晰的部分l評論員：評論員：

3、找缺陷，找缺陷，不討論解決方案不討論解決方案l記錄員：記錄員：記錄發(fā)現(xiàn)的錯誤，以及指派的任務記錄發(fā)現(xiàn)的錯誤，以及指派的任務l走查小組與代碼審查類似，但檢查方法不同走查小組與代碼審查類似，但檢查方法不同l測試者準備代表性的測試用例測試者準備代表性的測試用例l與會者與會者“充當充當”計算機，人工運行用例計算機，人工運行用例l許多錯誤在提問的過程中被發(fā)現(xiàn)許多錯誤在提問的過程中被發(fā)現(xiàn)9n驗證系統(tǒng)的正確性驗證系統(tǒng)的正確性l安全攸關(guān)系統(tǒng)、任務關(guān)鍵系統(tǒng)安全攸關(guān)系統(tǒng)、任務關(guān)鍵系統(tǒng)n分類分類l基于證明的驗證基于證明的驗證l模型檢測（模型檢測（Model CheckingModel Checking）10l系統(tǒng)：

4、邏輯公式集合系統(tǒng)：邏輯公式集合l規(guī)約：公式規(guī)約：公式 l驗證：驗證： ，即：即：可推導出可推導出 l一般需要用戶引導和專門知識一般需要用戶引導和專門知識n1980s早期由早期由Clarke 和和Emerson ，Queille 和和 Sifakis 獨立開發(fā)獨立開發(fā)2007年圖靈獎獲得者年圖靈獎獲得者開發(fā)模型檢測技術(shù)，并使之成為一個廣泛應用在硬件和軟件工業(yè)中非常有效的算法驗證技術(shù)所做的奠基性貢獻。12M模型檢驗器模型檢驗器p F qyesno反例反例n自動的、基于模型的、性質(zhì)驗證方法自動的、基于模型的、性質(zhì)驗證方法l 系統(tǒng)系統(tǒng)：有窮狀態(tài)模型：有窮狀態(tài)模型M（Kripke結(jié)構(gòu)）結(jié)構(gòu)）l 規(guī)約規(guī)約

5、/性質(zhì)性質(zhì)：時序邏輯：時序邏輯 l 驗證驗證： M ，即：，即： M是否滿足是否滿足 13n 3元組元組M = (S, T, L)l S：有窮狀態(tài)集：有窮狀態(tài)集l T S S：狀態(tài)遷移關(guān)系，滿足：狀態(tài)遷移關(guān)系，滿足 s S, s S (s, s) Tl L：S2AP：狀態(tài)標記函數(shù)。其中，：狀態(tài)標記函數(shù)。其中，AP為原子命題集，為原子命題集，L(s)表示狀態(tài)表示狀態(tài)s中為真的原子命中為真的原子命題集題集14AP：p, q, rS : s0, s1, s2T: (s0 , s1) , (s1 , s1) , (s2 , s1) , (s2 , s0) , (s0 , s2) L(s0) = p,

6、q L(s1) = q L(s2) = q, rp,qq,rqs0s1s2n示例示例16n路徑（路徑（path）一個無窮狀態(tài)序列：一個無窮狀態(tài)序列： = , i 1 (si, si+1） T路徑也表示為路徑也表示為：s1 s2 s3 i ：從：從si開始的后綴。如：開始的后綴。如： 3： s3 s4 17p,qq,rqs0s1s2p,qp,qs0q,rs2qs1qs1qs1s0qs1qs1q,rs2qs1路徑路徑n計算樹計算樹18n模型檢測回顧模型檢測回顧l 系統(tǒng)：有窮狀態(tài)模型系統(tǒng)：有窮狀態(tài)模型M（Kripke結(jié)構(gòu)）結(jié)構(gòu)）l 規(guī)約規(guī)約/性質(zhì)性質(zhì)：時序邏輯：時序邏輯 l 驗證：驗證： M ，即：

7、，即： M是否滿足是否滿足 在模型中，性質(zhì)公式的真值不是靜態(tài)的，當系統(tǒng)在模型中，性質(zhì)公式的真值不是靜態(tài)的，當系統(tǒng)從一個狀態(tài)到另一個狀態(tài)時，公式的真值會變化。從一個狀態(tài)到另一個狀態(tài)時，公式的真值會變化。19n線性時間邏輯線性時間邏輯l時間為路徑集合時間為路徑集合n分支時間邏輯分支時間邏輯l 時間表示為時間表示為“樹樹”20線性時序邏輯線性時序邏輯LTLLTLAmir Pnueli(1941-2009)The Weizmann Institute of Science 19961996年圖靈獎獲得者年圖靈獎獲得者把時態(tài)邏輯引入計算機科學把時態(tài)邏輯引入計算機科學的開創(chuàng)性工作，的開創(chuàng)性工作，以及在編程

8、語言和系統(tǒng)驗證方面的突出貢獻以及在編程語言和系統(tǒng)驗證方面的突出貢獻21nLTL : Linear-time Temporal LogicLTL : Linear-time Temporal Logicn語法語法 := | T T | p | ( ) | ( ) | ( ) | ( ) |X | G | F | U 其中，其中，p為原子命題，為原子命題， 為為LTL公式公式22n時序操作符時序操作符X ：下一狀態(tài)（：下一狀態(tài)（neXt）F ：某個將來（：某個將來（ Future）狀態(tài)）狀態(tài)G ：所有（：所有（Globally）將來狀態(tài)）將來狀態(tài)U ：直到（：直到（Until）23n優(yōu)先級優(yōu)先級一

9、元操作（一元操作（ 、X、F、G）兩元時序操作（兩元時序操作（ U 、R、W）邏輯運算符（邏輯運算符（ 、 ）邏輯運算符（邏輯運算符（）n例如例如F(p Gr) q U p =(F (p (G r) (q) U p)a a 在當前狀態(tài)為真在當前狀態(tài)為真aa a 在當前狀態(tài)為真在當前狀態(tài)為真X a a在下一個狀態(tài)為真在下一個狀態(tài)為真aa a 在當前狀態(tài)為真在當前狀態(tài)為真X a a在下一個狀態(tài)為真在下一個狀態(tài)為真Fa a在將來的某個狀態(tài)為真在將來的某個狀態(tài)為真aa a 在當前狀態(tài)為真在當前狀態(tài)為真X a a在下一個狀態(tài)為真在下一個狀態(tài)為真Fa a 在將來的某個狀態(tài)為真在將來的某個狀態(tài)為真Ga a

10、在將來的所有狀態(tài)為真在將來的所有狀態(tài)為真aaaaaaaaba a 在當前狀態(tài)為真在當前狀態(tài)為真X a a在下一個狀態(tài)為真在下一個狀態(tài)為真Fa a 在將來的某個狀態(tài)為真在將來的某個狀態(tài)為真Ga a 在將來的所有狀態(tài)為真在將來的所有狀態(tài)為真a U b a 為真直到為真直到 b變?yōu)檎孀優(yōu)檎?9n設(shè)：設(shè)：M = (S, T, L)， = s1 s2 |= T T, | |= aiff a L(s1) |= iff | |= 1 2iff |= 1 |= 2 |= 1 2 iff |= 1 |= 2 |= 1 2iff |= 1 |= 230 |= X iff 2|= |= G iff i 1 i |=

11、 |= F iff i 1 i |= |= 1 U 2 iff ( ( i 1 i |= 2) ) ( ( j 1, i ) j |= 1)31設(shè)模型設(shè)模型 M = (S, T, L)，s S，為為 LTL 公式公式，則：，則：M, s |= ，如果從如果從s開始的開始的每一條路徑每一條路徑 ， |= 32M, s0 |= X q M, s0 |= G (p r)M, s1 |= G qM, s0 |= p U qp,qp,qs0q,rs2qs1qs1q,rs2s0p,qq,rs2s0qs1q,rs2qs133n不可能到達一個狀態(tài)：不可能到達一個狀態(tài)：started成立成立ready 不成立不

12、成立G (started ready)n如果一個請求發(fā)生，它最終會被確認如果一個請求發(fā)生，它最終會被確認G (requested F acknowledged)n如果進程不時地（如果進程不時地（infinitely often）被使能，那被使能，那么就會不時地運行么就會不時地運行G F enabled G F runningn乘客要到乘客要到5 5樓，樓，2 2樓的向上電梯不會改變運行方向樓的向上電梯不會改變運行方向G(f2 up p5 (up U f5)34 G F ， F G X X F T T U ，G R W R ( ) R W ( )分配律分配律F ( ) F F ， 但但 F (

13、) F F G( ) G G ，但，但 G ( ) G G n互斥互斥安全性安全性(safety)(safety)：壞事永不發(fā)生：壞事永不發(fā)生任何時候只有一個進程處于臨界區(qū)任何時候只有一個進程處于臨界區(qū)活性活性(liveness)(liveness)：好事總會發(fā)生：好事總會發(fā)生只要請求進入臨界區(qū)，會被允許進入只要請求進入臨界區(qū)，會被允許進入無阻性無阻性(non-blocking)(non-blocking)進程總可以請求進入臨界區(qū)進程總可以請求進入臨界區(qū)非嚴格順序性非嚴格順序性無需按嚴格順序進入臨界區(qū)無需按嚴格順序進入臨界區(qū)n兩個進程：兩個進程： n n t t c c n n n n：處于非

14、臨界狀態(tài)處于非臨界狀態(tài)t t：試圖進入狀態(tài)試圖進入狀態(tài)c c：處于臨界狀態(tài)處于臨界狀態(tài)s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7n安全性：安全性：G G ( (c c1 1 c c2 2) )所有狀態(tài)滿足安全性所有狀態(tài)滿足安全性s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7n活性：活性：G(G(t t1 1 F F c c1 1) )s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7不滿足不滿足n無

15、阻性無阻性對所有滿足對所有滿足n1的狀態(tài)，的狀態(tài)，存在路徑存在路徑進入滿足進入滿足t1 的狀態(tài)的狀態(tài)s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7表達不了表達不了n非嚴格順序性非嚴格順序性存在路徑存在路徑，兩個滿足，兩個滿足c1的狀態(tài)的中間狀態(tài)的狀態(tài)的中間狀態(tài)都不滿足都不滿足c1和和c2s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7表達不了表達不了n重新建模重新建模n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s0s6s8s5n1 t2t1 t

16、2n1 c2t1 c2s7s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7G(t1 F c1)42nCTL (Computational tree logic)n語法語法 := | T T | p | ( ) | ( ) | ( ) | ( ) | AX | EX | AG | EG | AF | EF |A U | E U 其中，其中，p為原子命題，為原子命題， 為為CTLCTL公式公式43AX, EX, AG, EG, AU, AF, EFA ：所有（：所有（ All）路徑）路徑 inevitablyE ：存在：存在 （Exi

17、sts）一條路徑）一條路徑 possiblyX ：下一狀態(tài)（：下一狀態(tài)（neXt）F ：某個將來（：某個將來（ Future）狀態(tài)）狀態(tài)G ：所有（：所有（Globally）將來狀態(tài)）將來狀態(tài)U ：直到（：直到（Until）44n優(yōu)先級優(yōu)先級一元運算符：一元運算符： , AG, EG, AF, EF,AX, EX , , AU, EU45n EG rAG (q EG r) A p U EF r EF EG p AF rn EF (r U q) AF (r U q) (p U r)EF ggAF ggggAG ggggggggEG gggg50n設(shè)模型設(shè)模型M = (S, T, L), 路徑集路

18、徑集Path(M)M,s |= T T, M,s | , s SM,s |= piff p L(s)M,s |= iff M,s | M,s |= 1 2iff M,s |= 1 M,s |= 2M,s |= 1 2 iff M,s |= 1 M,s |= 2M,s |= 1 2iff M,s | 1 M,s |= 251M,s |= AX iff (s, s) T, M,s|= M,s |= EX iff (s, s) T, M,s|= M,s |= AG iff Path(M), s =s1, i 1 M,si |= M,s |= EG iff Path(M), s =s1, i 1 M,

19、si |= 52M,s |= AF iff Path(M), s =s1, i 1 M,si |= M,s |= EF iff Path(M), s =s1, i 1 M,si |= M,s |= A 1 U 2 iff Path(M), s =s1, i 1 M,si |= 2 j i M,sj |= 1 M,s |= E 1 U 2 iff Path(M), s =s1, i 1 M,si |= 2 j i M,sj |= 1 531) 不可能到達一個狀態(tài)：不可能到達一個狀態(tài)：started成立成立ready 不成立不成立2) 可能到達一個狀態(tài)：可能到達一個狀態(tài)：started成立成立re

20、ady 不成立不成立3) 如果一個請求發(fā)生，它最終會被確認如果一個請求發(fā)生，它最終會被確認4) 乘客要到乘客要到5 5樓，樓，2 2樓的向上電梯不會改變運行方向樓的向上電梯不會改變運行方向CTLCTLLTLLTL1)AG (started ready)G (started ready)2)EF (started ready)3)AG (requested AF acknowledged)G (requested F acknowledged)4)AG(f2 up p5 A(up U f5)G(f2 up p5 (up U f5)n直觀比較直觀比較CTL較強較強LTLLTL不能表達：任何狀態(tài)可以

21、到達不能表達：任何狀態(tài)可以到達 restart restart 狀態(tài)狀態(tài)CTLCTL表達：表達：AG EF restartLTL較強較強LTL可以描述在所有路徑上選擇一個范圍可以描述在所有路徑上選擇一個范圍F p F q：每條有：每條有p的路徑，也有的路徑，也有qAF p AF q和和AG( p AF q )含義都與之不同含義都與之不同n給定給定M = (S, T, L), s0 S和和 ，計算，計算M, s0 |= n若若M不滿足不滿足 ，產(chǎn)生反例，產(chǎn)生反例CTL的一個時態(tài)連接詞集合是充分的，當且僅當它至的一個時態(tài)連接詞集合是充分的，當且僅當它至少包含少包含AX, EX中之一，中之一，EG,

22、 AF, AU中之一以及中之一以及EU只考慮：只考慮： , , , , 和和AF, EU, EXAF, EU, EXn算法原理算法原理方法方法1輸入：輸入：M, s0 和和 輸出：輸出：yes或或no方法方法2輸入：輸入：M和和 輸出：滿足輸出：滿足 的狀態(tài)集的狀態(tài)集，檢查，檢查s0是否在該集合是否在該集合n標記算法標記算法 SAT( )輸入：輸入： M和和 輸出：滿足輸出：滿足 的狀態(tài)集合的狀態(tài)集合步驟步驟 轉(zhuǎn)換轉(zhuǎn)換 /只包含只包含 , , 和和AF, EU, EX 從從 中的原子命題開始直到中的原子命題開始直到 ，對每個子公式，對每個子公式 ，用用 標記使它滿足的所有狀態(tài)標記使它滿足的所有

23、狀態(tài) 輸出有標記輸出有標記 的所有狀態(tài)的所有狀態(tài)n計算計算 能標記狀態(tài)能標記狀態(tài) ：沒有任何狀態(tài)能帶標記：沒有任何狀態(tài)能帶標記 p：若：若p L(s)，則，則s 帶標記帶標記p 1 2：如果狀態(tài)：如果狀態(tài)s 同時帶標記同時帶標記 1和和 2，則，則可用可用 1 2標記標記s 1：如果狀態(tài)：如果狀態(tài)s 不帶不帶 1，則可標記，則可標記 1AF 1、狀態(tài)、狀態(tài)s 帶帶 ，則可標記，則可標記AF 2、若狀態(tài)、若狀態(tài)s的所有后繼狀態(tài)帶的所有后繼狀態(tài)帶AF ，則可用，則可用AF 標記標記s 。重。重復該過程，直到標記無變化復該過程，直到標記無變化 AF AF AF AF AF AF EX 如果狀態(tài)如果狀

24、態(tài)s有一個后繼狀態(tài)帶有一個后繼狀態(tài)帶 ，則，則s 可標記可標記EX EX E 1 U 21、狀態(tài)、狀態(tài)s 帶帶 2，則可標記，則可標記E 1 U 22、重復：若狀態(tài)、重復：若狀態(tài)s 帶帶 1并且至少一個后繼狀態(tài)帶并且至少一個后繼狀態(tài)帶E 1 U 2, 則則s 可標記可標記E 1 U 2 1E 1U 2 1E 1U 2E 1U 2 2E 1U 2n示例：互斥模型，示例：互斥模型，E c2 U c1是否滿足？是否滿足？n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s0s6s8s5n1 t2t1 t2n1 c2t1 c2s71, 標記標記c1n1 n2s3s2s1t1 n2c1

25、n2t1 t2c1 t2s4s0s6s8s5n1 t2t1 t2n1 c2t1 c2s72, 標記標記 c2n1 n2 c2s3s2s1t1 n2 c2c1 n2 c2t1 t2 c2c1 t2 c2s4s0s6s8s5n1 t2 c2t1 t2 c2n1 c2t1 c2s73, 標記標記E c2 U c1n1 n2 c2s3s2s1t1 n2 c2c1 n2 c2t1 t2 c2c1 t2 c2s4s0s6s8s5n1 t2 c2t1 t2 c2n1 c2t1 c2s7E c2 U c1E c2 U c13, 標記標記E c2 U c1n1 n2 c2s3s2s1t1 n2 c2c1 n2

26、c2t1 t2 c2c1 t2 c2s4s0s6s8s5n1 t2 c2t1 t2 c2n1 c2t1 c2s7E c2 U c1E c2 U c1E c2 U c13, 標記標記E c2 U c1n1 n2 c2s3s2s1t1 n2 c2c1 n2 c2t1 t2 c2c1 t2 c2s4s0s6s8s5n1 t2 c2t1 t2 c2n1 c2t1 c2s7E c2 U c1E c2 U c1E c2 U c1E c2 U c1E c2 U c1Function SAT( ) begincase is T T: return S is : return is atomic: return

27、 s S| L(s) is :return S - SAT( ) is 1 2 : return SAT( 1) SAT( 2) is 1 2 : return SAT( 1) SAT( 2) is 1 2 : return SAT( 1 2) is AF : return SATAF( ) is EF : return SAT (E U ) is AX : return SAT( EX ) is EX : return SATEX( ) is E 1 U 2 : return SATEU( 1, 2) is A 1 U 2 : return SAT ( (E 2 U ( 1 2) EG 2)

28、 is AG : return SAT ( EF ) is EG : return SAT( AF )end caseendFunction SATAF( ) Var X, YbeginX: = S;Y:=SAT( );repeat until X=YbeginX:=Y;Y:=Y pre (Y) endreturn Yendpre(Y) = s S | for all s, (s s implies s Y )Function SATEX( ) Var X, YbeginX:=SAT( );Y:=pre (X);return Yendpre (Y) = s S | exist s, (s s

29、and s Y )Function SATEU( , ) Var X, Y, WbeginX: = S;W:=SAT( );Y:=SAT( );repeat until X=YbeginX:=Y;Y:=Y (W pre (Y) ) endreturn Yendn標記算法的問題標記算法的問題對模型的規(guī)模是線性的對模型的規(guī)模是線性的模型規(guī)模隨變量個數(shù)成指數(shù)增長模型規(guī)模隨變量個數(shù)成指數(shù)增長狀態(tài)爆炸狀態(tài)爆炸克服狀態(tài)爆炸方法克服狀態(tài)爆炸方法 有序二叉決策圖有序二叉決策圖 符號模型檢測符號模型檢測 有界模型檢測有界模型檢測nLTLLTL的模型檢測算法比的模型檢測算法比CTLCTL的復雜的復雜1 1、CTL

30、CTL公式是在狀態(tài)上求值公式是在狀態(tài)上求值用狀態(tài)能滿足的子公式來標記系統(tǒng)的狀態(tài)用狀態(tài)能滿足的子公式來標記系統(tǒng)的狀態(tài)2 2、LTLLTL子公式不是在狀態(tài)上，而是沿著路徑求值子公式不是在狀態(tài)上，而是沿著路徑求值模型檢測必須采取不同的策略模型檢測必須采取不同的策略n問題問題給定給定M，s S 和和 ，計算計算M, s |= n基本策略基本策略1、為、為 構(gòu)造構(gòu)造接受接受 的自動機的自動機A 2、組合、組合A 和和M，即求兩者的公共路徑集合即求兩者的公共路徑集合3、搜索組合模型中是否存在從對應、搜索組合模型中是否存在從對應s 的狀態(tài)開的狀態(tài)開始的路徑始的路徑 存在：存在： M, s | 不存在：不存在

31、： M, s |= n示例示例M如圖如圖 ： (a U b)路徑：路徑： s3, s4, s3, s2, s2, 跡跡(trace)(trace)：a b, ab, a b, ab, ab, s2 a bs1 a bs4abs3a b1、構(gòu)造接受、構(gòu)造接受 (a U b)的自動機的自動機A a U bs2 ab s1 a b s4ab s 3a b s3a b =a U b2、合并合并A 和和M構(gòu)造構(gòu)造M的等價系統(tǒng)的等價系統(tǒng)s2 a bs1 a bs4abs3a bs2 a bs1 a bs4abs 3a bs3a b2、合并合并A 和和M合并（保留公共的遷移）合并（保留公共的遷移）s2 a bs1 a bs4abs 3a bs3a bs2 ab s1 a b s4ab s 3a b s3a b 2、合并合并A 和和Ms2 ab s1 a b s4ab s 3a b s3a b 3 3、搜索組合模型中是否存在從對應、搜索