《协议验证技术》PPT课件

《《协议验证技术》PPT课件》由会员分享，可在线阅读，更多相关《《协议验证技术》PPT课件（50页珍藏版）》请在金锄头文库上搜索。

1、第五章 协议验证分析技术5.1 概述概述 对协议本身的逻辑正确性进行校验的过程称之为验证对协议本身的逻辑正确性进行校验的过程称之为验证protocol verification.协议验证有两种途径：协议验证有两种途径：1协议分析协议分析protocol analysis2协议综合协议综合protocol synthesis 通常所说的协议验证指的是前者。协议综合将在第六通常所说的协议验证指的是前者。协议综合将在第六章讨论将协议设计过程和协议验证章讨论将协议设计过程和协议验证(分析分析)过程融合在一起，过程融合在一起，它通过一组能确保所设计的协议是正确的规那么，从一些根本它通过一组能确保所设计的

2、协议是正确的规那么，从一些根本协议模块中这些根本模块已证明是正确的产生所希望的目协议模块中这些根本模块已证明是正确的产生所希望的目标协议。标协议。 协议分析的目的是：对已设计的协议进行分析和校验协议分析的目的是：对已设计的协议进行分析和校验这些已设计的协议大都是采用非形式化设计方法产生的这些已设计的协议大都是采用非形式化设计方法产生的 第五章 协议验证技术协议分析包括许多方法，例如，1可达性分析reachability analysis2等价性分析equivalence analysis3不变性分析invariance analysis4符号执行symbol executin、模拟simula

3、tion等等。这些分析工作可以手动完成。 协议有多种表达形式，这包括：用自然语言描述的非形式化协议文本；用形式描述语言ESTELLE,LOTOS,SDL等描述的协议标准；用协议模型技术FSM，petrinet,CCS等表达的协议模型；以及用程序设计语言C，pascal等描述的协议代码。协议分析可在任何一种表达形式上进行，一般地说，上述所有方法都可在这几种表达形式上进行手工或软件工具。然而，除符号执行之外，人们都在协议模型上进行协议分析简单，容易形成确定算法。本章讨论三种分析方法，它们是可达性分析、不变性分析和等价分析。第五章 协议验证技术 5.2 可达性分析 可达性分析基于FSM模型技术试图产

4、生和检查协议所有或局部可达状态。所谓可达状态指协议从初始状态开始经历有限次转换之后可到达的状态，所有可达状态构成可达图reachability graph.可达性分析的最重要工作是产生和检查可达图，判定是否存在死锁，活锁等协议错误。可达性分析涉及三个重要技术：1怎样找到所有可达状态，构成可达图；2怎样检测死锁、活锁等协议错误；3怎样解决状态爆炸问题。第五章 协议验证技术5.2.1 穷尽可达性分析穷尽可达性分析 穷尽穷尽exnausive可达性分析产生和检可达性分析产生和检查所有协议状态。算法查所有协议状态。算法5.1描述了穷尽可达性描述了穷尽可达性分析的根本算法，该算法假定计算机的存储空分析的

5、根本算法，该算法假定计算机的存储空间足够大，计算速度足够高。间足够大，计算速度足够高。 第五章 协议验证技术算法5.1：exhausive reachability analysisstart()W=initial state;/工作集；将被分析的状态A=;/被分析过的状态analyze();/穷尽分析analyze()if (W=empty) return;q=last element from W;add q to A;find all successsors of q;if (q=error_state) report_error();else for each successor st

6、ate s of q if (s is not in A or W) add s to W; analyze(); delete q from W; 集合W包含未被分析的协议状态，A包含已分析和正在分析中的协议状态, 算法执行之前，W包含initial state,A为空，算法执行完毕之后,W为空，A包含协议的所有可达状态。该算法简单明了，然而要将它付诸实施时,我们还必须解决以下一些问题。第五章 协议验证技术1.状态表示方法协议状态用状态矩阵表示为:这里E1，E2，En，为n层协议的几个协议实体的局部状态，Cij为协议实体i到协议实体j的通道的状态。当所有通道可处理成空通道时，协议状态可用数组

7、E1,E2,En表示因为空通道只有一种状态。第五章 协议验证技术2.怎样找到所有可达的后继状态 不考虑报文顺序号，AB协议系统如图5.1所示，其中是R到S的通道，协议状态由二维矩阵组成。初始状态有四个后继状态：很显然，状态2，3和4不是可达状态(因为初始状态中AB内部没有任何数据需要传输，所以2，3),(4)状态是不可能出现的，即不可达的)。那么怎样判定1是可达状态，而2，3和4不是可达状态呢？第五章 协议验证技术AB协议系统第五章 协议验证技术为了解决这个问题，我们按下述格式定义交互事件： entity(state):actionpoint(state)?/!message这里，entity

8、(state)表示协议实体处于状态state中，action point(state)表示作用点处于状态state中，！表示发送，？表示接收。作用点的状态定义为“0或“1。发送！结束后，状态为“1；接收？结束后，状态为“0。AB协议系统有四个作用点，它们是用户和S之间接口A，用户和R之间接口B，S和通道之间接口a以及R和通道之间接口b。利用上述的事件表达格式，图5.1的事件表述如下：第五章 协议验证技术(7)R(1):b(0)!ack (8) R(1):B(0)!m(9)C12(0):a(1)?m (10)C12(1):drop(11)C12(1):b(0)!m (12)C21(0):b(1)

9、?ack(13)C21(1):a(0)!ack第五章 协议验证技术现在，我们就很容易判定初始状态下，事件l 可执行，而事件5 、9 和12 不会执行，这是因为初始化后，作用点状态分别是：A =l , B =0 , a =0 , b =0 利用作用点状态判定在协议状态q 之下，哪些事件会被执行，那么我们就可以找出q 的所有后继状态 第五章 协议验证技术3 改进方法去掉内部作用状态，而根据通道状态来判定哪些事件会被执行，将使算法变得简洁用这种方法时，外部作用点保存，通道内的事件隐藏起来AB 协议系统的事件简化为：S(0):A(1)?m (5)R(0):C12(1)?mS(1):C12(0)!m (

10、6)R(1):dropS(2):timeout (7)R(1):C21(0)!ackS(2):C21(1)?ack (8)R(1):B(0)!m通道内的事件无需表示出来，通道C12 的drop 事件盛加到事件6 中第五章 协议验证技术如果通道为队列通道，它的状态定义就会变得复杂，状态数也会激剧增加，事件的表述方法也变得复杂。例如，对于边界为n 的队列通道，事件表述形式可能为：entity(state):channel(staten)!message.就是说，当通道队列长度小于n 时，协议实体entity 才会执行报文发送事件。第五章 协议验证技术4 搜索方法算法5 . 1 的搜索方法取决于W

11、队列性质如果W 为FIFO 先进先出队列，搜索是按宽度优先breadth first进行的，如果W 为FILO 先进后出队列，搜索是按深度优先deapth first进行的深度优先搜索方法占用存贮空间小这是最大优点之一。假定每个状态有两个后继状态，算法执行m 步之后，对于深度优先搜索方法，W 的长度为m ，但对于宽度优先搜索，W 的长度为2m。第五章 协议验证技术5 ，状态爆炸和错误检测第三章在讨论FSM 简化时提到了什么是状态爆炸问题随着协议机制复杂性的提高和队列通道边界值的增大，状态爆炸问题使穷尽可达性分析变得无法实行讨论的非穷尽可达性分析技术力图解决这个问题算法5.1 中的语句：ifq=

12、error_statereport_error(),其内容非常丰富，实现比较困难。5 . 2 . 3 讨论各种协议错误的检侧方法。第五章 协议验证技术算法5 . 2 : start() W=initial state; A=; analyse(); analyse() If (W=empty) return; q =element from W; add q to A; find all successors of q; if (q = error_state) report_error(); else for some successor state s of q if (s is not

13、in A or W) add s to W analyse(); Delete q from W 5 . 2 . 2 非穷尽可达性分析将算法5 . 1 的语句for each successor state s of q 改为 for some successor state s of q, 其它语句不变，我们就得到非穷尽可达性分析算法第五章 协议验证技术 现在问题是，怎样从q 的所有后继状态中选取某些some状态进行分析，当然，被选取的状态应该是最有价值的，最有分析意义的，能最大可能检测协议错误的状态1 事件优先选择法事件t1,t2tn使状态q 产生n 个后继状态图5 . 2 ) ，如果给这

14、些事件赋于一定优先级别数值，那么被选择的后继状态一般只选择一个，应该是优先级别数高的事件产生的优先级别数值的赋值方法可以是：(1) 静态赋值 可达性分析进行之前，按照一定原那么发送事件优先于接收事件，协同事件高于内部事件等等对所有事件赋于静态优先数值，可达性分析过程中，这些数值不改变(2) 动态赋值 可达性分析执行之前，所有事件赋于相同的优先数值也可以不同，可达性分析过程中，事件每执行一次，其优先数减1 。这种方法可均衡各个事件的执行次数，使本来很少有时机执行的事件能尽快的执行一次。第五章 协议验证技术2 协议实体优先选择法协议实体优先选择法如果事件如果事件t1,t2tn是由多个不同协议实体执

15、行的，那么被是由多个不同协议实体执行的，那么被选择的后继状态应该是优先级别高的协议实体所执行的事件选择的后继状态应该是优先级别高的协议实体所执行的事件产生的协议实体的优先级别的赋值方法可以是：产生的协议实体的优先级别的赋值方法可以是：(1) 静态赋值静态赋值 按照一定原那么发方高于收方，响应方高于按照一定原那么发方高于收方，响应方高于发起方，发起方， ，等等赋给各个，等等赋给各个 协议实体优先数值，可达性分协议实体优先数值，可达性分析进行过程，数值不改变析进行过程，数值不改变(2) 动态赋值动态赋值 方法之一方法之一 按照执行事件的多少或最后一次执行按照执行事件的多少或最后一次执行事件的时间动

16、态改变协议实体的优先数值例如事件执行事件的时间动态改变协议实体的优先数值例如事件执行多的协议实体优先级别数降低，很长时间未执行任何事件的多的协议实体优先级别数降低，很长时间未执行任何事件的协议实体的优先级别数提高等等协议实体的优先级别数提高等等 动态斌值方法之二动态斌值方法之二 按照事件的相关特性动态调整协议实体的按照事件的相关特性动态调整协议实体的优先级别数值例如当协议实体优先级别数值例如当协议实体A 执行完发送事件之后，那执行完发送事件之后，那么执行该事件的协同事件的协议实体的优先数值就立即提高么执行该事件的协同事件的协议实体的优先数值就立即提高等等等等第五章 协议验证技术3 纯粹随机选择

17、法这是最简单而有效的选择方法：从q的n 个后继状态中任取1个或几个进行分析由于从q 的n 个后继状态中选择“最有分析价值的状态是一个不可判定的问题，因此纯悴随机选择方法是一种简单适用的方法。非穷尽可达性分析往往要进行屡次每次的状态选择方法不同才能得到较满意的结果第五章 协议验证技术5 .2.3 协议错误的检测方法 可达性分析可检侧死锁、活锁、无意义事件、非确定的输入事件等协议错误1如果q 无任何后继状态，那么q 就是死锁状态2 在穷尽可达性分析中，如果一个事件未被执行一次，那么该事件可判定为无意义事件 3对于非穷尽可达性分析，算法在执行一遍之后，如果某些事件未执行一次那么在第二遍执行中应将这些

18、事件的优先级别数值提高。只有当非穷尽可达性分析进行屡次之后，才能判定那些事件为无意义事件4 如果某个协议实体在执行输入事件之后所获取的报文不是它所期待的报文，那么这个事件为非确定输入事件非确定输入事件反映协议的完备性不好，即协议没有考虑异常报文的接收处理问题。第五章 协议验证技术6活锁死循环的检测是非常麻烦的事情活锁的检测首先是循环的检测在算法5 . 1 和5 . 2 中，如果q 的后继状态已在W 和A 中存在时，那么循环可能存在采用深度优先搜索方法时，循环容易检测这是深度优先搜索的优点之二：如果q 的后继状态s 已在W 中，那么s 到q 的状态序列依次排列在W 中这是一个循环作为一个案例分析

19、我们来检测图5 . 3 的循环，图中状态编号表示深度优先搜索过程中算法所访问的状态的先后次序状态5 有三个后继状态1 、3 ) 和6 ) . ( 6 不在W 中，它不构成循环后继状态3 在W 中，事件t3产生循环，循环序列为3 ) ( 4 ) ( 5 ) 后继状态1 在w 中，t1产生循环，循环序列为I ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) 深度优先搜索方法不但容易检测循环，而且很容易得出循环序列 第五章 协议验证技术 现在的问题是，上述方法能检测出所有循环吗？答案是否认的，例如，图5 . 3中t4，t5 ，t6和t7，产生的循环就检测不出来当算法执行到状态9 时，( 9 的后继

20、状态之一4 已不在W 中而是在A 中当算法执行到状态10 时，( 10 的后继状态6 也在A 中前者t4产生循环，后者t5不产生循环，这就说明，如果q 的后继状态在A 中，循环可能存在。第五章 协议验证技术当q的后继状态在A中时，判定它是否产生循环有两种方法。第五章 协议验证技术断点法算法执行多遍，执行第n遍算法时，将前面n1次算法已检测到的循环断开，以便检测新的循环。对于图5.3所示的系统，算法执行第一遍时，由t1，t2和t3产生的循环都能检测出来。执行第二遍算法的时断开34的转换，那么由t4产生的循环128945就检测出来了注意：第二次算法执行时，搜索顺序不同于第一次。执行第三次算法时再断

21、开89，那么由t6产生的循环12811945就检测出来了。第五章 协议验证技术n标记法n算法执行过程中，每检测到一个循环就给处于循环之中的状态打上“标记，说明它已处于某个循环之中。如果q的某个后续状态不在W中而在A中，并且它已处于某个循环之中，那么是否真正产生了新的循环，还必须做进一步判定。判定规那么是：如果q的后继状态s在A中，并且s已处于某个循环之中而且该循环序列的任何一个状态或几个仍然在W中，那么新的循环产生。图5.3中，当算法执行但状态9时，它的后继状态4在A中，并且已处于两个循环之中，这说明新的循环可能存在。由t3产生的循环的序列345中没有一个状态还处于W中，因此这个循环序列的所有

22、状态不包括在新的循环之中。由t1产生的循环序列12345中，1和2仍然处于W中，因此系ind循环序列存在，循环序列由12345组成。当算法执行到状态10时，虽然它的后继状态6在A中，但由于6未处于任何其他循环之中，因此不存在新的循环。 第五章 协议验证技术当所有循环已经检测出来之后，我们就可以判定那么循环是死循环。死循环的判定是更为复杂的问题。一种方法是通过“进展状态progress state的标记来确定一个循环是否为死循环。如果循环序列之内包含至少一个进展状态，那么它就不是死循环。进展状态的标记在可达性分析进行之前由手工进行。例如发送超时再发送构成一个循环，如果发送之前判定发送次数是否超过

23、给定数值超过给定值就转向错误处理，那么再发送状态就可以标记为进展状态。 第五章 协议验证技术5.3 不变性分析不变性分析如果一个系统的某个性质能用一个确定的逻辑表达式描述，如果一个系统的某个性质能用一个确定的逻辑表达式描述，并且恒为真不随系统的状态变化或执行序列而改变，那并且恒为真不随系统的状态变化或执行序列而改变，那么这个性质称为系统的不变性质，简称系统不变性。协议的么这个性质称为系统的不变性质，简称系统不变性。协议的不变性分析包括二个工作：第一是完全正确的找出系统协不变性分析包括二个工作：第一是完全正确的找出系统协议的不变性质。形成严格定义的不变性表达式；第二是以议的不变性质。形成严格定义

24、的不变性表达式；第二是以某种方式执行协议，验证不变性表达式是否恒为真。我们所某种方式执行协议，验证不变性表达式是否恒为真。我们所说的不变性分析指的是第二项工作。第一项工作由手工进行，说的不变性分析指的是第二项工作。第一项工作由手工进行，许多协议描述文本也包含了不变性表达式。许多协议描述文本也包含了不变性表达式。不变性分析可采用两种途径：第一是不变性证明系统往往不变性分析可采用两种途径：第一是不变性证明系统往往采用归纳法，第二是不变性监测系统。下面分别介绍它们。采用归纳法，第二是不变性监测系统。下面分别介绍它们。第五章 协议验证技术5.3.1 不变性证明系统不变性证明系统用归纳法证明一个数学公式

25、时，证明分两步进行：第一步证明x=0时公式是否成立；第二步，如果x=n时公式成立，那么证明x=n+1时公式是否成立。类似的，协议不变性证明也包括两步。首先，验证协议处于初始状态时不变性表达式是否成立，然后假设协议在某状态下不变性成立，验证协议从这个状态开始执行所有相关过程中不变性是否保持成立。我们以窗口流控制为例说明其证明过程，案例来自于文献资料【10】，本文已作剪辑。第五章 协议验证技术滑动窗口流控制是点对点通讯协议传输层，数据链路层所广泛采用的一种流控制方法。发送端维持两个计数器LW和HW，LW之值等于第一个未认可报文的顺序号，HW之值为下一次发送报文时能赋予的顺序号，HW和LW之间差为发

26、送窗口，窗口宽度不应大于给定值。所有为认可报文放入ACKQUE队列中，如果收到一个认可报文，发送端将已认可的报文从ACKQUE队列中擦去，并修改LW之值。接收端维持一个计数器NS，NS之值为下一个接受报文的顺序号。如果所接受的报文的顺序号不等于NS之值，丢弃该报文。假定报文顺序号为自然数并可以无限增大，那么对于这样一个窗口流控制，我们可形成3个不变性表达式：HW LW windowLW seq(element of ACKQUE) HWLW NS HW第五章 协议验证技术这里，window为窗口宽度的最大值，函数seq()的返回值为报文的顺序号。表达式1规定为认可报文的个数必须小于或等于win

27、dow，表达式2规定ACKQUE队列中的所有报文的顺序号应在窗口范围之内，表达式3规定接收端的NS总是在窗口之内。第五章 协议验证技术n为了用归纳法证明上述窗口流控制的不变性，我们必须罗列出协议中的所有相关的原子操作。这些原子操作包括：nSM:(Send a message)nIf( HW LW window)nn Seq(message) = HW;n HW = HW+1;n send the message;n put the message to ACKQUE;nnRA:(Receive an ack)nn if ( the ack is OK) and (LW = seq(ack) =

28、HW) n delete all message in ACKQUE with seq(message) seq(ack);n LW = seq(ack);nnRS:(RE send message after timeout)nSend all message in ACKQUE;nRM:(Receive a message)n If (the message is OK) and (seq(message) =NS)nn deliver the messsge to the user;n NS = NS + 1;nnSA:(Send the ack)nsend the ack with s

29、eq(ack) = NS;nTM:(Transmit a message over the channel)nthe message may be lost or destroyed;nTA:(Transmit an ack over the channel)nThe ack may be lost or destroyed;第五章 协议验证技术原子操作SM，RA和RS由发端协议实体执行，RM和SA由收端协议实体执行，TM和TA由通道执行。不变性1和2的证明比较简单，因为只涉及发端协议实体所执行的原子操作。下面用归纳法证明不变性3。证明：第一步初始化后，HW = 0,LW = 0, NS =

30、0因此LW=NS=HW,表达式3成立。第二步假定协议在执行到某个状态时HW=j，LW=i，NS=k，并且ikj成立。验证发端协议实体发出一个新的报文之后，协议在执行所有相关原子操作之后，表达式3是否成立。SM SM发出顺序号为j的报文之后，HW= j+1，LWNSHW,表达式3成立TM TM不改变HW，LW和NS的值；第五章 协议验证技术RS 如果超时事件产生，重发报文，RS不修改HW,LW和NS；RM 由于SM执行之后HW=j+1，当RM执行之后，虽然NS=K+1，但表达式3仍然成立。如果所接收的报文顺序号有错，RM不修改NS，因此表达式3成立；SA 不改变 HW,LW和NSTA 不修改HW

31、,LW和NS,TA发出的ACK报文的顺序号为k到j之间任意数值，即seq(ck)=kj；RA 正确执行之后LW=NS=seq(ck)=kj,而HW仍然为j+1，因此表达式3成立。如果RA丢弃ack报文，HW,LW和NS不变。证毕。第五章 协议验证技术n5.3.2 不变性监测系统不变性监测系统 n不变性监测系统借助监测软件和监测方法对模拟运行不变性监测系统借助监测软件和监测方法对模拟运行或符号执行中的协议进行不变性校验的过程称之为不或符号执行中的协议进行不变性校验的过程称之为不变性监测变性监测invariant monitoring。这种方法要求。这种方法要求在协议代码中插入断点子程序的调用或返

32、回可视为在协议代码中插入断点子程序的调用或返回可视为自然断点，每个断点处，监测系统取相关变量值，自然断点，每个断点处，监测系统取相关变量值，计算并校验不变性表达式是否成立。除此之外，监测计算并校验不变性表达式是否成立。除此之外，监测程序还可以对程序断言程序还可以对程序断言assert进行校验，程序断进行校验，程序断言是嵌于协议代码指定地方的特殊语句，例如言是嵌于协议代码指定地方的特殊语句，例如ASSERT(state= =1)。协议代码运行到。协议代码运行到ASSERT语语句时将指示监测程序对句时将指示监测程序对assert语句所申明的布尔表达语句所申明的布尔表达式进行校验。不变性表达式不同于

33、程序断言之处在于式进行校验。不变性表达式不同于程序断言之处在于它无需插入协议代码之中。它无需插入协议代码之中。第五章 协议验证技术n无论是不变性证明系统还是监测系统，我们都认为下述两个问题都是不可判定问题。n不变性表达式已完整、准确、严密地表述了协议的所有行为和性质吗？n用归纳法证明不变性时，引用的原子操作已覆盖了所有相关操作吗？在监测系统中，所设立的断点完备吗？n在通过监测系统进行不变性分析时，我们还遇到一个麻烦问题。协议系统由多个协议实体组成分布式，监测系统必须凌驾于它们之上，实现起来比较困难。由于上述这些问题和愿因，不变性分析在协议验证中的应用受到很大限制。第五章 协议验证技术5.4 等

34、价性分析等价性分析“等价意味着某种程度上的等价意味着某种程度上的“相同和相同和“无差异。如果两个协无差异。如果两个协议模型或协议标准是等价的，那么它们可以互相替换，如果一个是议模型或协议标准是等价的，那么它们可以互相替换，如果一个是正确的，那么另一个也是正确的。我们在第三章讨论正确的，那么另一个也是正确的。我们在第三章讨论FSM和和CCS时时已利用已利用“等价方法简化等价方法简化FSM图和图和CCS表达式，这实质上也是一种表达式，这实质上也是一种等价性分析方法。等价性分析的另一个途径是证明两个协议的等价性分析方法。等价性分析的另一个途径是证明两个协议的FSM图或图或CCS表达式是等价的，典型的

35、情况是证明协议标准和它的效劳表达式是等价的，典型的情况是证明协议标准和它的效劳标准一致性。标准一致性。按等价的含义和等价的强弱，等价性分为【按等价的含义和等价的强弱，等价性分为【20】：】：1 观察等价观察等价observational equivalence如果对两个协议进行状态到状态的互相模拟时所观察到的协议行为如果对两个协议进行状态到状态的互相模拟时所观察到的协议行为没有差异，这两个协议是观察等价的。本节重点讨论观察等价性。没有差异，这两个协议是观察等价的。本节重点讨论观察等价性。2 测试等价测试等价test equivalence如果对两个协议施加相同的测试序列所观察到的协议行为没有差

36、异，如果对两个协议施加相同的测试序列所观察到的协议行为没有差异，那么这两个协议是测试等价的。那么这两个协议是测试等价的。第五章 协议验证技术3 跟踪等价trace equivalence如果两个协议执行的事件序列是相同的，那么它们是踪迹等价的。4 实现等价implementation equivalence如果一个协议所做的每一件事情都能被第二个模仿mimic，反之亦然，那么它们是实现等价的。这四种等价按强弱程度排列的话，顺序是：观察等价、测试等价、跟踪等价、实现等价，其中观察等价还分为强观察等价和弱观察等价。等价性的强弱反映两个协议对行为细节的相同程度，等价性越强，它们的行为细节的相同程度越

37、高。第五章 协议验证技术5.4.1 基于基于FSM的观察等价性分析的观察等价性分析 对于状态转换系统对于状态转换系统参见第三章参见第三章3.2节，定义节，定义S*S为状态映射集合，例如，一个包括三个状态为状态映射集合，例如，一个包括三个状态S0、S1和和S2的的FSM，S*S包括九种映射：包括九种映射：S0 ，S0，S1 ，S1，S2 ，S2，S0 ，S1S2 ，S1。下面研究一。下面研究一种特殊映射种特殊映射互拟关系。互拟关系。如果两个状态如果两个状态pS，qS能够互相模拟，那么能够互相模拟，那么p,q为互为互拟关系拟关系bisimulation relation。互拟关系分强互拟关系。互拟

38、关系分强互拟关系strong bisimulation relation和弱互拟关系和弱互拟关系weak bisimulation relation4，13，它们的定义如下：，它们的定义如下：1 强状态互拟关系：强状态互拟关系：状态转换系统状态转换系统的两个状态的两个状态pS，qS为强互拟为强互拟关系的充分必要条件是，对所有关系的充分必要条件是，对所有eE：第五章 协议验证技术 如果存在一个pS，p pT，那么就一定存在一个qS，qqT，并且p,q为强互拟关系； 如果存在一个qS，q qT，那么就一定存在一个pS，p pT，并且p,q为强互拟关系；2 弱状态互拟关系：状态转换系统的两个状态pS

39、，qS为弱互拟关系的充分必要条件是，对所有eE，e不为I内部事件； 如果存在一个pS，p pT，那么就一定存在一个qS，q qT，并且p,q为弱互拟关系； 如果存在一个qS，q qT，那么就一定存在一个pS，p pT，并且p,q为弱互拟关系；第五章 协议验证技术第五章 协议验证技术第五章 协议验证技术 图5.4和图5.5所示的例子中，我们可以得出这样的一个结论，即强互拟关系和弱互拟关系的差异在于后者忽略了内部事件。两个状态为强互拟关系就一定为弱互拟关系，反之不然。一个FSM中所有强状态互拟关系的集合为FSM的强互拟关系RS，RS是S*S的一个子集。一个FSM中所有弱状态互拟关系的集合为FSM的

40、弱互拟关系RW，RW是S*S的一个子集，并且RW大于RS。图5.4所示的FSM的RW等于RS，图5.5的RS=1,1,2,2,3,3,4,4,5,5，而RW=RS+2,3。第五章 协议验证技术 互拟关系特别是弱互拟关系有两种重要应用，一是FSM的简化，二是两个FSM的等价性比较即等价性分析。1 FSM的简化 如果p,q为的一对弱状态互拟关系，那么p，q可合并成一个状态，FSM得到简化。第3章节在讨论FSM的简化方法四隐藏内部事件时，我们已经给出假设干简化FSM的例子图3.5图3.7。第五章 协议验证技术FSM的等价比较我们真正感兴趣的是两个FSM是否等价，两个FSM的等价分强互拟等价stron

41、g bisimulation equivalence和弱互拟等价weak bisimulation equivalence，它们分别可借助于FSM的强互拟关系和弱互拟关系来定义。强互拟等价：两个相同和为强互拟等价的充分必要条件是： 第五章 协议验证技术上述定义弱互拟等价为例可解释为：为了证明两个系统是否弱互拟等价，我们只要将两个系统和起来看作一个系统，找出复合系统的弱互拟关系Rw，并且证明两个初始状态为弱状态互拟关系就可以了。条件2有嵌套性，即如果(i1,i2)为弱状态互拟关系，那么它们的后继状态一定是弱状态互拟关系参见FSM的弱状态互拟关系定义，同样，它们的后继状态的后继状态一定是弱互拟关系

42、因此两个系统的所有状态一定是彼此为弱互拟关系。根据这个原理，我们可以设计一个算法，建立一个自动证明系统去证明两个FSM是否等价。第五章 协议验证技术在许多文献中，两个FSM的强弱互拟等价也称之为强弱观察等价strong/weak observation equivalence)。图5.6的两个FSM是弱观察等价的，它们的复合系统的弱互拟关系Rw为：Rw(.,(),(0,(0,.),(0,(.,0),(00,(0,0),(1,(1,.),(1,(.,1),(11,(1,1),(10,(1,0),(01,(0,1)它们初始状态(.,(.,.)是弱状态互拟的，读者可验证各对互拟状态是否成立，案例来自

43、【20】。第五章 协议验证技术FSM的弱观察等价的弱观察等价第五章 协议验证技术5.4.2 基于基于CCS的观察等价性分析的观察等价性分析上节定义的观察等价性可直接引入到CCS表达式。两个系统的行为表达式两个系统的行为表达式B1和和B2是强观察是强观察等价的充分必要条件是它们对应的状态转换等价的充分必要条件是它们对应的状态转换系统是强观察等价的，同样，表达式系统是强观察等价的，同样，表达式B1和和B2是弱观察等价的充分必要条件是它们对应的是弱观察等价的充分必要条件是它们对应的FSM是观察等价的。是观察等价的。怎样根据CCS表达式导出FSM呢？第五章 协议验证技术第五章 协议验证技术 观察等价是CCS和LOTOS的理论根底，它们所形成的代数变换规那么有的基于强观察等价性，有的基于弱观察等价行。CCS或LOTOS表达式变换过程就是等价变换过程。第三章第5节已给出了多个CCS表达式的实例，此处不再重复。