第8講模型檢測(cè)

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

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

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

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

5、構(gòu)）l 規(guī)約規(guī)約/性質(zhì)性質(zhì)：時(shí)序邏輯：時(shí)序邏輯 l 驗(yàn)證驗(yàn)證： 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)標(biāo)記函數(shù)。其中，：狀態(tài)標(biāo)記函數(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(s

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

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

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

9、n優(yōu)先級(jí)優(yōu)先級(jí)1. 一元操作（一元操作（ 、X、F、G）2. 兩元時(shí)序操作（兩元時(shí)序操作（ U 、R、W）3. 邏輯運(yùn)算符（邏輯運(yùn)算符（ 、 ）4. 邏輯運(yùn)算符（邏輯運(yùn)算符（）n例如例如F(p Gr) q U p =(F (p (G r) (q) U p)a a 在當(dāng)前狀態(tài)為真在當(dāng)前狀態(tài)為真aa a 在當(dāng)前狀態(tài)為真在當(dāng)前狀態(tài)為真X a a在下一個(gè)狀態(tài)為真在下一個(gè)狀態(tài)為真aa a 在當(dāng)前狀態(tài)為真在當(dāng)前狀態(tài)為真X a a在下一個(gè)狀態(tài)為真在下一個(gè)狀態(tài)為真Fa a在將來的某個(gè)狀態(tài)為真在將來的某個(gè)狀態(tài)為真aa a 在當(dāng)前狀態(tài)為真在當(dāng)前狀態(tài)為真X a a在下一個(gè)狀態(tài)為真在下一個(gè)狀態(tài)為真Fa a 在將來的某

10、個(gè)狀態(tài)為真在將來的某個(gè)狀態(tài)為真Ga a 在將來的所有狀態(tài)為真在將來的所有狀態(tài)為真aaaaaaaaba a 在當(dāng)前狀態(tài)為真在當(dāng)前狀態(tài)為真X a a在下一個(gè)狀態(tài)為真在下一個(gè)狀態(tài)為真Fa a 在將來的某個(gè)狀態(tài)為真在將來的某個(gè)狀態(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 1. |= T T, | 2. |= aiff a L(s1)3. |= iff | 4. |= 1 2iff |= 1 |= 25. |= 1 2 iff |= 1 |= 26. |= 1 2iff |= 1 |=

11、 2307. |= X iff 2|= 8. |= G iff i 1 i |= 9. |= F iff i 1 i |= 10. |= 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開始的開始的每一條路徑每一條路徑 ， |= 321. M, s0 |= X q 2. M, s0 |= G (p r)3. M, s1 |= G q4. M, s0 |= p U qp,qp,qs0q,rs2qs1qs1q,rs2s0p,qq,r

12、s2s0qs1q,rs2qs133n不可能到達(dá)一個(gè)狀態(tài)：不可能到達(dá)一個(gè)狀態(tài)：started成立成立ready 不成立不成立G (started ready)n如果一個(gè)請(qǐng)求發(fā)生，它最終會(huì)被確認(rèn)如果一個(gè)請(qǐng)求發(fā)生，它最終會(huì)被確認(rèn)G (requested F acknowledged)n如果進(jìn)程不時(shí)地（如果進(jìn)程不時(shí)地（infinitely often）被使能，那被使能，那么就會(huì)不時(shí)地運(yùn)行么就會(huì)不時(shí)地運(yùn)行G F enabled G F runningn乘客要到乘客要到5 5樓，樓，2 2樓的向上電梯不會(huì)改變運(yùn)行方向樓的向上電梯不會(huì)改變運(yùn)行方向G(f2 up p5 (up U f5)34 G F ， F

13、G X X F T T U ，G R W R ( ) R W ( )分配律分配律F ( ) F F ， 但但 F ( ) F F G( ) G G ，但，但 G ( ) G G n互斥互斥安全性安全性(safety)(safety)：壞事永不發(fā)生：壞事永不發(fā)生任何時(shí)候只有一個(gè)進(jìn)程處于臨界區(qū)任何時(shí)候只有一個(gè)進(jìn)程處于臨界區(qū)活性活性(liveness)(liveness)：好事總會(huì)發(fā)生：好事總會(huì)發(fā)生只要請(qǐng)求進(jìn)入臨界區(qū)，會(huì)被允許進(jìn)入只要請(qǐng)求進(jìn)入臨界區(qū)，會(huì)被允許進(jìn)入無阻性無阻性(non-blocking)(non-blocking)進(jìn)程總可以請(qǐng)求進(jìn)入臨界區(qū)進(jìn)程總可以請(qǐng)求進(jìn)入臨界區(qū)非嚴(yán)格順序性非嚴(yán)格順序性

14、無需按嚴(yán)格順序進(jìn)入臨界區(qū)無需按嚴(yán)格順序進(jìn)入臨界區(qū)n兩個(gè)進(jìn)程：兩個(gè)進(jìn)程： n n t t c c n n n n：處于非臨界狀態(tài)處于非臨界狀態(tài)t t：試圖進(jìn)入狀態(tài)試圖進(jìn)入狀態(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

15、n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7不滿足不滿足n無阻性無阻性對(duì)所有滿足對(duì)所有滿足n1的狀態(tài)，的狀態(tài)，存在路徑存在路徑進(jìn)入滿足進(jìn)入滿足t1 的狀態(tài)的狀態(tài)s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7表達(dá)不了表達(dá)不了n非嚴(yán)格順序性非嚴(yán)格順序性存在路徑存在路徑，兩個(gè)滿足，兩個(gè)滿足c1的狀態(tài)的中間狀態(tài)的狀態(tài)的中間狀態(tài)都不滿足都不滿足c1和和c2s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7表達(dá)不了表達(dá)不了

16、n重新建模重新建模n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s0s6s8s5n1 t2t1 t2n1 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,

17、 EG, AU, AF, EFA ：所有（：所有（ All）路徑）路徑 inevitablyE ：存在：存在 （Exists）一條路徑）一條路徑 possiblyX ：下一狀態(tài)（：下一狀態(tài)（neXt）F ：某個(gè)將來（：某個(gè)將來（ Future）狀態(tài)）狀態(tài)G ：所有（：所有（Globally）將來狀態(tài)）將來狀態(tài)U ：直到（：直到（Until）44時(shí)序邏輯操作符時(shí)序邏輯操作符n優(yōu)先級(jí)優(yōu)先級(jí)一元運(yùn)算符：一元運(yùn)算符： , 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

18、(r U q) (p U r)CTL: CTL: 示例示例EF ggCTL: CTL: 示例示例AF ggggCTL: CTL: 示例示例AG ggggggggCTL: CTL: 示例示例EG gggg50n設(shè)模型設(shè)模型M = (S, T, L), 路徑集路徑集Path(M)1.M,s |= T T, M,s | , s S2.M,s |= piff p L(s)3.M,s |= iff M,s | 4.M,s |= 1 2iff M,s |= 1 M,s |= 25.M,s |= 1 2 iff M,s |= 1 M,s |= 26.M,s |= 1 2iff M,s | 1 M,s |=

19、2517.M,s |= AX iff (s, s) T, M,s|= 8.M,s |= EX iff (s, s) T, M,s|= 9.M,s |= AG iff Path(M), s =s1, i 1 M,si |= 10.M,s |= EG iff Path(M), s =s1, i 1 M,si |= 5211.M,s |= AF iff Path(M), s =s1, i 1 M,si |= 11.M,s |= EF iff Path(M), s =s1, i 1 M,si |= 13.M,s |= A 1 U 2 iff Path(M), s =s1, i 1 M,si |= 2

20、j i M,sj |= 1 14.M,s |= E 1 U 2 iff Path(M), s =s1, i 1 M,si |= 2 j i M,sj |= 1 531) 不可能到達(dá)一個(gè)狀態(tài)：不可能到達(dá)一個(gè)狀態(tài)：started成立成立ready 不成立不成立2) 可能到達(dá)一個(gè)狀態(tài)：可能到達(dá)一個(gè)狀態(tài)：started成立成立ready 不成立不成立3) 如果一個(gè)請(qǐng)求發(fā)生，它最終會(huì)被確認(rèn)如果一個(gè)請(qǐng)求發(fā)生，它最終會(huì)被確認(rèn)4) 乘客要到乘客要到5 5樓，樓，2 2樓的向上電梯不會(huì)改變運(yùn)行方向樓的向上電梯不會(huì)改變運(yùn)行方向CTLCTLLTLLTL1)AG (started ready)G (started r

21、eady)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較強(qiáng)較強(qiáng)LTLLTL不能表達(dá)：任何狀態(tài)可以到達(dá)不能表達(dá)：任何狀態(tài)可以到達(dá) restart restart 狀態(tài)狀態(tài)CTLCTL表達(dá)：表達(dá)：AG EF restartLTL較強(qiáng)較強(qiáng)LTL可以描述在所有路徑上選擇一個(gè)范圍可以描述在所有路徑上選擇一個(gè)范圍F p F q：每條有：每條有p的路徑，也有的路徑，也有qAF p A

22、F q和和AG( p AF q )含義都與之不同含義都與之不同n給定給定M = (S, T, L), s0 S和和 ，計(jì)算，計(jì)算M, s0 |= n若若M不滿足不滿足 ，產(chǎn)生反例，產(chǎn)生反例CTL的一個(gè)時(shí)態(tài)連接詞集合是充分的，當(dāng)且僅當(dāng)它至的一個(gè)時(shí)態(tài)連接詞集合是充分的，當(dāng)且僅當(dāng)它至少包含少包含AX, EX中之一，中之一，EG, AF, AU中之一以及中之一以及EU只考慮：只考慮： , , , , 和和AF, EU, EXAF, EU, EXn算法原理算法原理方法方法1輸入：輸入：M, s0 和和 輸出：輸出：yes或或no方法方法2輸入：輸入：M和和 輸出：滿足輸出：滿足 的狀態(tài)集的狀態(tài)集，檢查，

23、檢查s0是否在該集合是否在該集合n標(biāo)記算法標(biāo)記算法 SAT( )輸入：輸入： M和和 輸出：滿足輸出：滿足 的狀態(tài)集合的狀態(tài)集合步驟步驟 轉(zhuǎn)換轉(zhuǎn)換 /只包含只包含 , , 和和AF, EU, EX 從從 中的原子命題開始直到中的原子命題開始直到 ，對(duì)每個(gè)子公式，對(duì)每個(gè)子公式 ，用用 標(biāo)記使它滿足的所有狀態(tài)標(biāo)記使它滿足的所有狀態(tài) 輸出有標(biāo)記輸出有標(biāo)記 的所有狀態(tài)的所有狀態(tài)n計(jì)算計(jì)算 能標(biāo)記狀態(tài)能標(biāo)記狀態(tài) ：沒有任何狀態(tài)能帶標(biāo)記：沒有任何狀態(tài)能帶標(biāo)記 p：若：若p L(s)，則，則s 帶標(biāo)記帶標(biāo)記p 1 2：如果狀態(tài)：如果狀態(tài)s 同時(shí)帶標(biāo)記同時(shí)帶標(biāo)記 1和和 2，則，則可用可用 1 2標(biāo)記標(biāo)記s

24、1：如果狀態(tài)：如果狀態(tài)s 不帶不帶 1，則可標(biāo)記，則可標(biāo)記 1AF 1、狀態(tài)、狀態(tài)s 帶帶 ，則可標(biāo)記，則可標(biāo)記AF 2、若狀態(tài)、若狀態(tài)s的所有后繼狀態(tài)帶的所有后繼狀態(tài)帶AF ，則可用，則可用AF 標(biāo)記標(biāo)記s 。重。重復(fù)該過程，直到標(biāo)記無變化復(fù)該過程，直到標(biāo)記無變化 AF AF AF AF AF AF EX 如果狀態(tài)如果狀態(tài)s有一個(gè)后繼狀態(tài)帶有一個(gè)后繼狀態(tài)帶 ，則，則s 可標(biāo)記可標(biāo)記EX EX E 1 U 21、狀態(tài)、狀態(tài)s 帶帶 2，則可標(biāo)記，則可標(biāo)記E 1 U 22、重復(fù)：若狀態(tài)、重復(fù)：若狀態(tài)s 帶帶 1并且至少一個(gè)后繼狀態(tài)帶并且至少一個(gè)后繼狀態(tài)帶E 1 U 2, 則則s 可標(biāo)記可標(biāo)記E

25、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, 標(biāo)記標(biāo)記c1n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s0s6s8s5n1 t2t1 t2n1 c2t1 c2s72, 標(biāo)記標(biāo)記 c2n1 n2 c2s3s2s1t1 n2 c2c1 n2 c2t1 t2 c2c1 t2 c2s4s0s6s8s5n1 t2 c2t1 t2 c2n1 c2t1 c2s7

26、3, 標(biāo)記標(biāo)記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, 標(biāo)記標(biāo)記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 c13, 標(biāo)記標(biāo)記E c2 U c1n1 n2 c2s3s2s1t1 n2 c2c1 n2 c2t1 t2 c2c

27、1 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 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

28、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) 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:

29、=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 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標(biāo)記算法的問題

30、標(biāo)記算法的問題對(duì)模型的規(guī)模是線性的對(duì)模型的規(guī)模是線性的模型規(guī)模隨變量個(gè)數(shù)成指數(shù)增長(zhǎng)模型規(guī)模隨變量個(gè)數(shù)成指數(shù)增長(zhǎng)狀態(tài)爆炸狀態(tài)爆炸克服狀態(tài)爆炸方法克服狀態(tài)爆炸方法 有序二叉決策圖有序二叉決策圖 符號(hào)模型檢測(cè)符號(hào)模型檢測(cè) 有界模型檢測(cè)有界模型檢測(cè)nLTLLTL的模型檢測(cè)算法比的模型檢測(cè)算法比CTLCTL的復(fù)雜的復(fù)雜1 1、CTLCTL公式是在狀態(tài)上求值公式是在狀態(tài)上求值用狀態(tài)能滿足的子公式來標(biāo)記系統(tǒng)的狀態(tài)用狀態(tài)能滿足的子公式來標(biāo)記系統(tǒng)的狀態(tài)2 2、LTLLTL子公式不是在狀態(tài)上，而是沿著路徑求值子公式不是在狀態(tài)上，而是沿著路徑求值模型檢測(cè)必須采取不同的策略模型檢測(cè)必須采取不同的策略n問題問題給定給定

31、M，s S 和和 ，計(jì)算計(jì)算M, s |= n基本策略基本策略1、為、為 構(gòu)造構(gòu)造接受接受 的自動(dòng)機(jī)的自動(dòng)機(jī)A 2、組合、組合A 和和M，即求兩者的公共路徑集合即求兩者的公共路徑集合3、搜索組合模型中是否存在從對(duì)應(yīng)、搜索組合模型中是否存在從對(duì)應(yīng)s 的狀態(tài)開的狀態(tài)開始的路徑始的路徑 存在：存在： M, s | 不存在：不存在： 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)的自動(dòng)機(jī)的自動(dòng)機(jī)A a U bs2 ab s1 a b s4ab s 3a b s3a b =a U b2、合并合并A 和和M構(gòu)造構(gòu)造M的等價(jià)系統(tǒng)的等價(jià)系統(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、搜