5协议验证技术(ok).ppt

第五章 协议验证技术 5.3.1 不变性证明系统 用归纳法证明一个数学公式时，证明分两步进行：第一步证明x=0时公式是否成立；第二步，如果x=n时公式成立，那么证明x=n+1时公式是否成立。类似的，协议不变性证明也包括两步。首先，验证协议处于初始状态时不变性表达式是否成立，然后假设协议在某状态下不变性成立，验证协议从这个状态开始执行所有相关过程中不变性是否保持成立。 我们以窗口流控制为例说明其证明过程，案例来自于文献资料【10】，本文已作剪辑。 第五章 协议验证技术 滑动窗口流控制是点对点通讯协议（传输层，数据链路层）所广泛采用的一种流控制方法。发送端维持两个计数器LW和HW，LW之值等于第一个未认可报文的顺序号，HW之值为下一次发送报文时能赋予的顺序号，HW和LW之间差为发送窗口，窗口宽度不应大于给定值。所有未认可报文放入ACKQUE队列中，如果收到一个认可报文，发送端将已认可的报文从ACKQUE队列中擦去，并修改LW之值。接收端维持一个计数器NS，NS之值为下一个接受报文的顺序号。如果所接受的报文的顺序号不等于NS之值，丢弃该报文。假定报文顺序号为自然数并可以无限增大，那么对于这样一个窗口流控制，我们可形成3个不变性表达式： HW — LW window LW seq(element of ACKQUE) HW LW NS HW 第五章 协议验证技术 这里，window为窗口宽度的最大值，函数seq()的返回值为报文的顺序号。表达式1规定未认可报文的个数必须小于或等于window，表达式2规定ACKQUE队列中的所有报文的顺序号应在窗口范围之内，表达式3规定接收端的NS总是在窗口之内。 第五章 协议验证技术 SM:(Send a message) If( HW － LW window) { Seq(message) = HW; HW = HW+1; send the message; put the message to ACKQUE; } RA:(Receive an ack) { if (( the ack is OK) and (LW = seq(ack) =HW)) delete all message in ACKQUE with seq(message) seq(ack); LW = seq(ack); } RS:(RE— send message after timeout-) Send all message in ACKQUE; RM:(Receive a message) If ((the message is OK) and (seq(message) ==NS)) { deliver the messsge to the user; NS = NS + 1; } SA:(Send the ack) send the ack with seq(ack) = NS; TM:(Transmit a message over the channel) the message may be lost or destroyed; TA:(Transmit an ack over the channel) The ack may be lost or destroyed; 为了用归纳法证明上述窗口流控制的不变性，我们必须罗列出协议中的所有相关的原子操作。这些原子操作包括： 第五章 协议验证技术 原子操作SM，RA和RS由发端协议实体执行，RM和SA由收端协议实体执行，TM和TA由通道执行。不变性1和2的证明比较简单，因为只涉及发端协议实体所执行的原子操作。下面用归纳法证明不变性3。 证明： 第一步 初始化后，HW = 0,LW = 0, NS = 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和NS TA 不修改HW,LW和NS,TA发出的ACK报文的顺序号为k到