第8讲模型检测

1、u白盒测试和黑盒测试白盒测试和黑盒测试u静态测试静态测试和动态测试（和动态测试（验证测试和确认测试验证测试和确认测试）u传统测试方法和面向对象测试的方法传统测试方法和面向对象测试的方法直接检查源代码或其它文档l同行评审同行评审l桌面检查桌面检查l代码审查代码审查l走查走查l软件验证软件验证l也称好友评审也称好友评审l不是很正式：不是很正式：“你把你的拿给我看看，我把你把你的拿给我看看，我把我的拿给你看看我的拿给你看看”l由软件设计和编码人员加上一两个其它程序由软件设计和编码人员加上一两个其它程序员或测试人员组成员或测试人员组成l对源程序代码进行人工分析、检验对源程序代码进行人工分析、检验l关注

2、变量值和程序逻辑关注变量值和程序逻辑l记录检查结果记录检查结果l最好由非程序作者本人模拟执行程序最好由非程序作者本人模拟执行程序l只有一个人在阅读代码，没有团队协作只有一个人在阅读代码，没有团队协作5示例示例l软件业最佳实践软件业最佳实践l重点放在查找工作产品缺陷上重点放在查找工作产品缺陷上l文档必须通过质量关卡（文档必须通过质量关卡（核对表，核对表，ChecklistChecklist）n角色l主持人：主持人：控制进度，分派和跟踪任务，报告审查结果控制进度，分派和跟踪任务，报告审查结果l作者：作者：陈述项目的概况，解释代码中不清晰的部分陈述项目的概况，解释代码中不清晰的部分l评论员：评论员：

3、找缺陷，找缺陷，不讨论解决方案不讨论解决方案l记录员：记录员：记录发现的错误，以及指派的任务记录发现的错误，以及指派的任务l走查小组与代码审查类似，但检查方法不同走查小组与代码审查类似，但检查方法不同l测试者准备代表性的测试用例测试者准备代表性的测试用例l与会者与会者“充当充当”计算机，人工运行用例计算机，人工运行用例l许多错误在提问的过程中被发现许多错误在提问的过程中被发现9n验证系统的正确性验证系统的正确性l安全攸关系统、任务关键系统安全攸关系统、任务关键系统n分类分类l基于证明的验证基于证明的验证l模型检测（模型检测（Model CheckingModel Checking）10l系统：

4、逻辑公式集合系统：逻辑公式集合l规约：公式规约：公式 l验证：验证： ，即：即：可推导出可推导出 l一般需要用户引导和专门知识一般需要用户引导和专门知识n1980s早期由早期由Clarke 和和Emerson ，Queille 和和 Sifakis 独立开发独立开发2007年图灵奖获得者年图灵奖获得者开发模型检测技术，并使之成为一个广泛应用在硬件和软件工业中非常有效的算法验证技术所做的奠基性贡献。12M模型检验器模型检验器p F qyesno反例反例n自动的、基于模型的、性质验证方法自动的、基于模型的、性质验证方法l 系统系统：有穷状态模型：有穷状态模型M（Kripke结构）结构）l 规约规约

5、/性质性质：时序逻辑：时序逻辑 l 验证验证： M ，即：，即： M是否满足是否满足 13n 3元组元组M = (S, T, L)l S：有穷状态集：有穷状态集l T S S：状态迁移关系，满足：状态迁移关系，满足 s S, s S (s, s) Tl L：S2AP：状态标记函数。其中，：状态标记函数。其中，AP为原子命题集，为原子命题集，L(s)表示状态表示状态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）一个无穷状态序列：一个无穷状态序列： = , i 1 (si, si+1） T路径也表示为路径也表示为：s1 s2 s3 i ：从：从si开始的后缀。如：开始的后缀。如： 3： s3 s4 17p,qq,rqs0s1s2p,qp,qs0q,rs2qs1qs1qs1s0qs1qs1q,rs2qs1路径路径n计算树计算树18n模型检测回顾模型检测回顾l 系统：有穷状态模型系统：有穷状态模型M（Kripke结构）结构）l 规约规约/性质性质：时序逻辑：时序逻辑 l 验证：验证： M ，即：

7、，即： M是否满足是否满足 在模型中，性质公式的真值不是静态的，当系统在模型中，性质公式的真值不是静态的，当系统从一个状态到另一个状态时，公式的真值会变化。从一个状态到另一个状态时，公式的真值会变化。19n线性时间逻辑线性时间逻辑l时间为路径集合时间为路径集合n分支时间逻辑分支时间逻辑l 时间表示为时间表示为“树树”20线性时序逻辑线性时序逻辑LTLLTLAmir Pnueli(1941-2009)The Weizmann Institute of Science 19961996年图灵奖获得者年图灵奖获得者把时态逻辑引入计算机科学把时态逻辑引入计算机科学的开创性工作，的开创性工作，以及在编程

8、语言和系统验证方面的突出贡献以及在编程语言和系统验证方面的突出贡献21nLTL : Linear-time Temporal LogicLTL : Linear-time Temporal Logicn语法语法 := | T T | p | ( ) | ( ) | ( ) | ( ) |X | G | F | U 其中，其中，p为原子命题，为原子命题， 为为LTL公式公式22n时序操作符时序操作符X ：下一状态（：下一状态（neXt）F ：某个将来（：某个将来（ Future）状态）状态G ：所有（：所有（Globally）将来状态）将来状态U ：直到（：直到（Until）23n优先级优先级一

9、元操作（一元操作（ 、X、F、G）两元时序操作（两元时序操作（ U 、R、W）逻辑运算符（逻辑运算符（ 、 ）逻辑运算符（逻辑运算符（）n例如例如F(p Gr) q U p =(F (p (G r) (q) U p)a a 在当前状态为真在当前状态为真aa a 在当前状态为真在当前状态为真X a a在下一个状态为真在下一个状态为真aa a 在当前状态为真在当前状态为真X a a在下一个状态为真在下一个状态为真Fa a在将来的某个状态为真在将来的某个状态为真aa a 在当前状态为真在当前状态为真X a a在下一个状态为真在下一个状态为真Fa a 在将来的某个状态为真在将来的某个状态为真Ga a

10、在将来的所有状态为真在将来的所有状态为真aaaaaaaaba a 在当前状态为真在当前状态为真X a a在下一个状态为真在下一个状态为真Fa a 在将来的某个状态为真在将来的某个状态为真Ga a 在将来的所有状态为真在将来的所有状态为真a U b a 为真直到为真直到 b变为真变为真29n设：设：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设模型设模型 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不可能到达一个状态：不可能到达一个状态：started成立成立ready 不成立不

12、成立G (started ready)n如果一个请求发生，它最终会被确认如果一个请求发生，它最终会被确认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)：坏事永不发生：坏事永不发生任何时候只有一个进程处于临界区任何时候只有一个进程处于临界区活性活性(liveness)(liveness)：好事总会发生：好事总会发生只要请求进入临界区，会被允许进入只要请求进入临界区，会被允许进入无阻性无阻性(non-blocking)(non-blocking)进程总可以请求进入临界区进程总可以请求进入临界区非严格顺序性非严格顺序性无需按严格顺序进入临界区无需按严格顺序进入临界区n两个进程：两个进程： n n t t c c n n n n：处于非

14、临界状态处于非临界状态t t：试图进入状态试图进入状态c c：处于临界状态处于临界状态s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7n安全性：安全性：G G ( (c c1 1 c c2 2) )所有状态满足安全性所有状态满足安全性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的状态，的状态，存在路径存在路径进入满足进入满足t1 的状态的状态s0n1 n2s3s2s1t1 n2c1 n2t1 t2c1 t2s4s6s5n1 t2n1 c2t1 c2s7表达不了表达不了n非严格顺序性非严格顺序性存在路径存在路径，两个满足，两个满足c1的状态的中间状态的状态的中间状态都不满足都不满足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 ：下一状态（：下一状态（neXt）F ：某个将来（：某个将来（ Future）状态）状态G ：所有（：所有（Globally）将来状态）将来状态U ：直到（：直到（Until）44n优先级优先级一元运算符：一元运算符： , 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设模型设模型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) 不可能到达一个状态：不可能到达一个状态：started成立成立ready 不成立不成立2) 可能到达一个状态：可能到达一个状态：started成立成立re

20、ady 不成立不成立3) 如果一个请求发生，它最终会被确认如果一个请求发生，它最终会被确认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不能表达：任何状态可以

21、到达不能表达：任何状态可以到达 restart restart 状态状态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不满足不满足 ，产生反例，产生反例CTL的一个时态连接词集合是充分的，当且仅当它至的一个时态连接词集合是充分的，当且仅当它至少包含少包含AX, EX中之一，中之一，EG,

22、 AF, AU中之一以及中之一以及EU只考虑：只考虑： , , , , 和和AF, EU, EXAF, EU, EXn算法原理算法原理方法方法1输入：输入：M, s0 和和 输出：输出：yes或或no方法方法2输入：输入：M和和 输出：满足输出：满足 的状态集的状态集，检查，检查s0是否在该集合是否在该集合n标记算法标记算法 SAT( )输入：输入： M和和 输出：满足输出：满足 的状态集合的状态集合步骤步骤 转换转换 /只包含只包含 , , 和和AF, EU, EX 从从 中的原子命题开始直到中的原子命题开始直到 ，对每个子公式，对每个子公式 ，用用 标记使它满足的所有状态标记使它满足的所有

23、状态 输出有标记输出有标记 的所有状态的所有状态n计算计算 能标记状态能标记状态 ：没有任何状态能带标记：没有任何状态能带标记 p：若：若p L(s)，则，则s 带标记带标记p 1 2：如果状态：如果状态s 同时带标记同时带标记 1和和 2，则，则可用可用 1 2标记标记s 1：如果状态：如果状态s 不带不带 1，则可标记，则可标记 1AF 1、状态、状态s 带带 ，则可标记，则可标记AF 2、若状态、若状态s的所有后继状态带的所有后继状态带AF ，则可用，则可用AF 标记标记s 。重。重复该过程，直到标记无变化复该过程，直到标记无变化 AF AF AF AF AF AF EX 如果状态如果状

24、态s有一个后继状态带有一个后继状态带 ，则，则s 可标记可标记EX EX E 1 U 21、状态、状态s 带带 2，则可标记，则可标记E 1 U 22、重复：若状态、重复：若状态s 带带 1并且至少一个后继状态带并且至少一个后继状态带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标记算法的问题标记算法的问题对模型的规模是线性的对模型的规模是线性的模型规模随变量个数成指数增长模型规模随变量个数成指数增长状态爆炸状态爆炸克服状态爆炸方法克服状态爆炸方法 有序二叉决策图有序二叉决策图 符号模型检测符号模型检测 有界模型检测有界模型检测nLTLLTL的模型检测算法比的模型检测算法比CTLCTL的复杂的复杂1 1、CTL

30、CTL公式是在状态上求值公式是在状态上求值用状态能满足的子公式来标记系统的状态用状态能满足的子公式来标记系统的状态2 2、LTLLTL子公式不是在状态上，而是沿着路径求值子公式不是在状态上，而是沿着路径求值模型检测必须采取不同的策略模型检测必须采取不同的策略n问题问题给定给定M，s S 和和 ，计算计算M, s |= n基本策略基本策略1、为、为 构造构造接受接受 的自动机的自动机A 2、组合、组合A 和和M，即求两者的公共路径集合即求两者的公共路径集合3、搜索组合模型中是否存在从对应、搜索组合模型中是否存在从对应s 的状态开的状态开始的路径始的路径 存在：存在： 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、构造接受、构造接受 (a U b)的自动机的自动机A a U bs2 ab s1 a b s4ab s 3a b s3a b =a U b2、合并合并A 和和M构造构造M的等价系统的等价系统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、搜索组合模型中是否存在从对应、搜索