（计算机科学与技术专业论文）基于属性的层次移动ipv6hmipv6协议的验证.pdf

原创性声明 i i i i iii ii iii ll u l li i i i i i i y 18 8 7 4 5 7 本人声明：所呈交的学位论文是本人在导师的指导下进行的研究工作及取得的研究成果。 除本文己经注明引用的内容外，论文中不包含其他人己经发表或撰写过的研究成果，也不包 含为获得囱苤直太堂及其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对 本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。 学位论文作者签名： 攀竖 指导教师签名： 日期： 2 2 丝：12 日期： 、 ， 、刀产一 杉毛 2 忽f 7门 在学期间研究成果使用承诺书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：内蒙古大学有权将 学位论文的全部内容或部分保留并向国家有关机构、部门送交学位论文的复印件和磁盘，允 许编入有关数据库进行检索，也可以采用影印、缩印或其他复制手段保存、汇编学位论文。 为保护学院和导师的知识产权，作者在学期间取得的研究成果属于内蒙古大学。作者今后使 用涉及在学期间主要研究内容或研究成果，须征得内蒙古大学就读期间导师的同意；若用于 发表论文，版权单位必须署名为内蒙古大学方可投稿或公开发表。 、 ， 学位论文作者签名：篷坌聋指导教师签名：空簦兰鱼 日 期：2 翻：z ：12 日期： 互4 l ：12 内蒙古大学硕士学位论文 基于属性的层次移动i p v 6 ( h m i p v 6 ) 协议的验证 摘要 随着互联网的高速发展，网络协议标准也不断地更新和完善。如何更有效 地提高网络服务，已成为网络协议工程领域的关键问题之一。层次移动i p v 6 协 议作为移动i p v 6 协议的扩展，在移动i p v 6 的基础上对移动节点在小范围内快速 切换作出了改进。 c p n ( c o l o u r e dp e t r in e t s ) 是一种形式化建模语言，适用于通信和并发系统。 c p n 为使用者提供了直观的图形化的形式化描述方法，并且c p n 的模型语言是 通用目的的建模语言。 本文通过形式化方法对自然语言描述的h m i p v 6 ( 砌5 3 8 0 ) 协议规范进行 建模，并对h m i p v 6 协议的基本属性进行形式化验证。由于协议并发行为引发 的状态爆炸问题严重影响了验证工作的进行，本文提出了模型化简和抽象的方 法，化简法将模型化检为多个并发子模型，抽象法将并发子模型进行抽象层次 的提升，合并二些库所和变迁，以减少状态空间规模，保证属性验证工作的效 果。最后，本文将以上方法应用于h m i p v 6 协议模型，验证了方法的有效性。 关键词：h m i p v 6 协议，形式化建模，c o l o u r e dp e t r in e t s ，属性，形式化验证，模型 检测 基于属性的层次移动口v 6 ( h m 口v 6 ) 协议的验证 h m i p v 6f o r 压alv e r 【f i c a t i o nr e s e a r c hb a s e do nc o l o r p e t r in e t s a b s t r a c t w 油t h e r a p i dd e v e l o p m e n to fi n t c r n c t ，n e t w o r kp r o t o c o ls t a n d a r d sa r ec o n s t a n t l yu p d a t e da n d i m p r o v e d h o wt oe f f e c t i v e l yi m p r o v et h en e t w o r ks e r v i c e sh a sb e c o m eo n eo fk e yp r o b l e m so ft h e n e t w o r kp r o t o c o le n g i n e e r i n gf i e l d a sa ne x t e n s i o no fm o b i l ei p v 6 ( m i p v 6 ) ，h i e r a r c h i c a lm o b i l e i p v 6 ( h m i p v 6 ) i sm a d et oi m p r o v et h e 【n ( m o b i l en o d e s ) f a s t m o v i n gi nas m a l lr a n g er e g i o n b a s e do nm i p v 6 ( m o b i l ei p v 6 ) ： c p n ( c o l o u r e dp e t r in e t s ) i saf o r m a lm o d e l i n gl a n g u a g e ，w h i c hi ss u i t a b l ef o rd e s c r i b i n ga s y s t e mw i t hc o n c u r r e n c ya n dc o m m u n i c a t i o n t h ec p np r o v i d e saf o r m a ld e s c r i p t i o nm e t h o d ， w h i c hi sm o r ei n t u i t i v ea n d g r a p h i c a l f o r t h eu s e r s a n dt h ec p n m o d e l i n gl a n g u a g e i sa g e n e r a l p u r p o s em o d e l i n gl a n g u a g e 。 ： i nt h i st h e s i s ，af o r m a lm o d e li sg i v e nf o rt h eh m 口v 6p r o t o c o lw h i c hh a sb e e nd e s c r i p t i o nb y n a t u r a ll a n g u a g e ，a n dt h eb a s i cp r o p e r t i e so fh m i p v 6p r o t o c o lm o d e li sv e r i f i e d b e c a u s eo ft h e s t a t ee x p l o s i o np r o b l e mc a u s e db yc o n c u r r e n tb e h a v i o r , v e r i f i c a t i o nh a sb e e nh i n d e r e d s oa s i m p l i f i e da n da b s t r a c tm e t h o di sp r e s e n t e d b yt h i sm e t h o d ，t h em o d e li ss i m p l i f i e di n t om u l t i p l e c o n c u r r e n ts u b - m o d e l s ，a n dt h ea b s t r a c t i o nl e v e lo fc o n c u r r e n ts u b - m o d e l si si m p r o v e d ，s o m eo ft h e p l a c e sa n dt r a n s i t i o n sa l em e r g e d s ot h es t a t es p a c ei sr e d u c e da n das o u n dv e r i f i c a t i o ne f f e c ti s g a i n e d f i n a l l y , t h e s em e t h o di s u s e do nh m 口v 6m o d e l ，t h ee f f e c t i v e n e s so ft h i sm e t h o di s t e s t i f i e d k e y w o r d s ：h m i p v 6 ，f o r m a lm o d e l i n g ，c o l o u r e dp c t r in e t s ，p r o p e r t y , m o d e lc h e c k i n g ， f o r m a lv e r i f i c a t i o n 3 4 1t o p 层建模：- 1 1 3 4 2 h a 层建模：，。1 2 3 4 3c n 层建模1 2 3 4 4m a p 层建模1 3 3 4 5a r s 层建模1 4 3 4 6m n 层建模。1 5 3 4 7r e a t r 层建模1 6 3 5 本章小结：1 7 第4 章基础属性的验证。1 8 4 1 微移动属性验证1 8 i i i 基于属性的层次移动口v 6 ( h m i p v 6 ) 协议的验证 4 1 1 验证属性1 8 4 1 2 模拟执行：1 9 4 1 3 结果分析2 1 4 2 宏移动属性验证：2 2 4 2 1 验证属性2 2 4 2 2 模拟执行分析。2 3 4 2 3 结果分析2 4 4 3 通信节点c n 向移动节点m n 发送数据2 6 4 3 1 验证属性2 6 4 3 2 模拟执行分析，2 7 4 3 3 结果分析：2 8 4 4 移动节点m n 向通信节点c n 发送数据。3 0 4 4 1 验证属性3 0 4 4 2 模拟执行方法分析3 0 4 4 3 结果分析：31 4 5 本章小结：。3 3 。 第5 章模型的并发属性验证_ ：3 4 5 1 保持所关注的基本属性的模型化简与抽象方法3 4 5 1 1 模型化简。3 5 5 1 2 模型抽象3 5 5 2h m i p v 6 模型的化简和抽象3 8 5 2 一分析h m i p v 6 协议的模型说明3 8 5 2 2 生成子模型：3 9 5 2 3 对子模型进行合并，提升抽象层次3 9 5 3h m i p v 6 协议模型并发属性的验证4 3 5 3 1 “微移动”和“微移动”并发。4 3 5 3 2 “宏移动”和“宏移动”并发4 8 5 3 3 一微移动”和“数据消息”并发。5 2 5 3 4 “宏移动”和“数据消息”并发：5 5 5 4对比分析5 7 i v v 图4 1 发送路由广播_ 1 9 图4 2 判断消息类型1 9 图4 3 发送绑定信息。2 0 图4 4 更新并发送a c k 消息2 0 图4 5 确认绑定信息2 0 图4 6 “微移动”完全状态空间：2 1 图4 7 “微移动”变迁点火序列2 2 v i 内蒙古大学硕士学位论文 图4 8a s k c t l 检测“微移动”2 2 图4 9 发送h a b u i 2 4 图4 1 0 绑定h a b u ：2 4 图4 1 1 “宏移动”完全状态空间2 5 一 图4 1 2 “宏移动”点火变迁序列2 5 图4 1 3a s k c t l 检测“宏移动9 5oeeooeoeoe ：2 6 图4 1 4 发送数据包2 7 图4 1 5 转发数据包一上：2 7 图4 1 6 封装数据包并转发_ 。2 8 图4 1 7 存储数据包一2 8 图4 1 8 “c n 向m n 传输数据”完全状态空间图2 9 图4 1 9 “c n 向m n 传输数据”变迁点火序列。：。2 9 一 图4 2 0a s k c t l 检测“c n 向移动节点m n 发送数据”2 9 图4 2 1m n 向c n 发送数据。31 图4 2 2 取出数据并转发给c n ：31 图4 2 3m n 收到数据包并存储31 图4 2 4 “c n 向m n 传输数据”完全状态空间图：“3 2 图4 2 5 “c n 向m n 传输数据”点火序列：3 2 图4 2 6a s k c t l 检测“m n 向移动节点c n 发送数据”3 3 图5 1 路径种类。j 3 6 图5 2 直路例子：3 6 图5 3 情况2 ，分解j 。3 7 图5 4 情况4 ，特例3 8 图5 5 可合并的直路3 9 图5 6 修改后的r e s t r 4 0 图5 7 a r s 中的合并路径j “4 1 图5 8a r s 中合并后的路径：4 1 。 图5 9m n 中分解路径4 2 图5 1 0 合并后的r e s t r 模块k j 4 2 图5 1 1 “微移动”并发初始条件4 4 v 内蒙古大学硕士学位论文 1 1 研究背景 第1 章引言 随着互联网的飞速发展和便携式移动终端的不断增加，以及宽带无线局域网技术的不断 完善，用户越来越希望能够随时随地的加入到互联网中获取如同固定接入一样的服务质量。 这种潜在的巨大商业需求给互联网带来了新的机遇与新的难题。i e t f 在2 0 0 4 年公布了移动 i p v 6 的标准r f c 3 7 7 5 1 1 。移动i p v 6 是在当前网络前提下，使移动节点在不同网络间移动时能 保持通信。移动i p v 6 的设计目标就是使得移动节点通过一个永久的i p v 6 地址就能连接到任 何一个网络上，并且在网络间切换时能保证通信不被中断。移动i p v 6 具有可扩展性、可靠性 和安全性，并且移动口v 6 工作于网络层，可以在不同的链路层上使用，同时对网络层以上也 是透明的，不仅适用于同种介质网络间的移动，也适用于异种介质网络间的移动，所以有广 阔的应用前景。 但是，根据1 e t f 的移动i p v 6 规范( r f c 3 7 7 5 ) ，当移动节点接入外地网络后，需要向家乡 代理进行注册，在收到家乡代理的绑定注册确认后才能开始通信。而且，移动节点还需要向 通信节点进行注册。如此，当移动结点快速移动时，由于移动结点需要在家乡代理和通信结 点之间传递大量的绑定更新报文，而它们可能相距较远，因此会产生严重的丢包和延时等问 题。 如何提高移动节点的移动性能，如何更好的为客户提供服务成为了移动i p v 6 发展的主要 问题。因此，为了更好的处理快速切换时更新报文频繁问题，引入了h m i p v 6 2 】。层次移动 i p v 6 ( h m i p v 6 ) 作为移动口v 6 的一种改进技术用于解决快速切换管理问题。h m i p v 6 在m i p v 6 的基础上，在引入了一个新的实体移动锚点( m a p ) ，对现有网络进行了区域化的划分， 从而将移动结点的移动区分为“宏移动”和“微移动”。当m n 发生“微移动”时，只向m a p 发送 绑定更新，更新信息不会发送到m a p 外部，减少绑定更新报文，从而提高网络传输数据的 效率，同时可以实现域内的快速切换。 目前i e t f 制定的i n t e r n e t 协议标准r f c 仍使用自然语言描述。随着网络的飞速发展以及 对服务性要求的提高，网络系统越来越复杂，靠传统软件工程方法设计出的协议很难满足我 们的要求。而协议实现后纠正错误的代价十分高昂，因此产生了形式化方法。形式化方法是 传统的软件工程方法的重要补充，它可以提高自动化的程度和更高的可靠性。形式化方法的 主要内容包括两个方面：形式化规约，形式化验证。形式化规约有多种方式：逻辑、自动机、 对h m i p v 6 的研究方向已经有了很多：层次化移动i p v 6 中宏微移动的快速切换，基于 层次移动口v 6 接入认证设计与实现，快速层次移动i p v 6 切换性能及其优化，基于h m i p v 6 的域间无缝切换方案等，但对h m i p v 6 协议的验证并没有很多。验证可以检查出一些对系统 存在危害的潜在问题，在协议的实现前尽可能找出更多的问题，为软件的实现降低潜在危险1 2 0 0 3 年启动的中国下一代互联网示范工程( c n g i 项目) 是国家级的战略项目j 由八部委 。 联合发起并经国务院批准启动，该项目的主要目的是搭建下一代互联网的试验平台，i p v 6 是 其中要采用的一项重要技术，标志着我国i p v 6 商用化进程进入了实质性发展阶段。i p v 6 对下 一代网络和3 g 网络的影响巨大。 2 内蒙古大学硕士学位论文 1 3 研究内容和主要工作 、 本文主要使用c p nt o o l s 对h m i p v 6 ( r f c 5 3 8 0 ) 协议进行建模，然后使用模型检测的方 法对协议进行验证。 本文的主要工作和贡献包括下面几个方面： 本文对h m i p v 6 协议进行了形式化建模及分析。本文采用层次化的方法对h m i p v 6 协 议进行形式化建模，通过c p nt o o l s 使得h m i p v 6 协议模型更加简洁、直观、形象。 对h m i p v 6 协议模型的基本属性进行分析验证。本文对h m i p v 6 协议的基本属性进行 分析，并采用模拟执行等方法分别对各个基本属性进行验证，给出正确模型。 本文提出了化简和抽象的方法，通过生成多个子模型来覆盖与模型的所有并发情况， 以子模型代替原模型进行相关并发属性的验证，并保证了方法的可行性，为研究协议 复杂情况下的并发属性提供了可能。 使用给出的方法对h m i p v 6 协议模型进行化简和抽象，对新生成的子模型通过模拟执 行、状态空间分析和a s k c t l 模型检验分析等方法保证协议所有并发属性的正确性， 并且验证了模型满足协议要求。一 1 4 论文结构 本文的其余部分可分为五章。第二章对h m i p v 6 协议进行了概述，并对c p n 以及本文 使用的c p nt o o l s 进行了简要介绍；第三章对h m i p v 6 协议进行了形式化建模，描述了模型 各个模块的设计以及功能；第四章对h m i p v 6 协议模型的基本属性进行验证。首先对模型的 基本属性进行划分，然后用模拟执行、状态空间分析等方法对基本属性分别进行验证；第五 章对h m i p v 6 协议模型进行化简和抽象，并对新模型的并发属性进行验证。本章首先给出了 一种化简和抽象复杂模型的方法，能够有效的减小模型规模，从而对并发属性进行验证。然 后用给出的方法对h m i p v 6 协议模型进行验证。第六章对本文的工作进行总结，并对下一步 工作进行展望。 3 基于属性的层次移动口v 6 ( h m i p v 6 ) 协议的验证 第2 章背景知识 本章对相关的背景知识进行了简要介绍。对h m i p v 6 协议进行了简要说明，并对本文主 要使用的c p n 和c p n t o o l s 进行了介绍。 2 1h m i p v 6 协议简介 移动i p v 6 协议中没有说明如何优化移动节点在切换过程中的性能。流畅的通信在于减小 切换过程中的延时，即快速切换；连续的通信在于减少切换过程中的丢包率，即平滑切换。 层次化移动i p v 6 在每个区域内定义了一个新的实体移动锚点( m a p ) ，改进了最基 本的移动m v 6 切换方案m a p 把切换过程分成微观移动和宏观移动。在h m i p v 6 中，移动 节点分配了两个地址，区域转交地址( r c o a ，r e g i o n a lc a r eo f a d d r e s s ) 和链路转交地址 ( l c o a ，o nl i n kc a r eo f a d d r e s s ) ，这两个地址在宏观移动和微观移动中非常有用。宏观移动 和微观移动逻辑结构图如图2 1 所示。当m n 从p a r l 处移动到p a r 2 处的时候，为微移动， 由m a p 充当本地的家乡代理，此时绑定更新过程只需要在p a r l 、p a r 2 、m a p 、m n 之间 进行，并且绑定更新过程完全对h a 和c n 透明；而当m n 继续从p a r 2 移动到n a r 的时候， 为宏移动，此时绑定更新过程和移动口v 6 一样，需要h a 、c n 的参与。 图2 1h m 口v 6 基本架构 f i g u r e2 1h m i p v 6b a s i cs t r u c t i o n 用分级的思想区别小区域移动与大区域移动是非常适合互联网的，因为这样有以下两个 明显的优点：第一，它提高了切换性能，因为小区域切换被限制在了一个很小的网络范围内， 所以，它可以加快切换的速度、减少切换时的丢包率。第二，它明显的减少了网络中的切换 管理信令，避免了网络中的信息拥塞，。这是因为，在一个域内的移动，它的切换信令不会传 4 内蒙古大学硕士学位论文 送到整个网络中去。 2 2c p n 简介 c o l o u r e dp e t r in e t s ( c p n e t s 或c p n s ) 是一种形式化建模语言，适用于通信、同步、及资 源共享系统。c p n s 3 】【4 1 为使用者提供了直观的图形化的形式化描述方法。c p n 的模型语言是 通用目的的建模语言，它并不只适用于一类系统而是面向广泛的系统并可以描述并发系统。 它的典型的应用领域包括通信协议、数据网络、分布式算法、嵌入式系统，在工业领域也有 很多应用。 这里先给出c p n 和层次化c p n 的形式化定义： 定义1 c o l o u r e dp e t r in e t 是一个九元组c p n = ( p ，t ，a ，s ，vc ，1 3 ie ，i ) ，其中： 1 p 是一个有限的库所( p l a c e ) 的集合。 ， 2 t 是一个有限变迁的集合，且t 满足p nt = 矽。 3 a 口p x tut p 是有向弧的集合。 4 s 是有限非空c o l o rs e t 类型的集合。 5 v 是有限变量的集合，对所有变量v v 满足t y p e v 】s 。 6 c ：p _ 是c o l o rs e t 函数，它给每个位置分配一个ac o l o rs e t 。 7 g ：t - * e x p r v 是防卫表达式，每个变迁有一个防卫表达式，例如：t y p e e g ( t ) 】= b o o l 。 8 e ：a - e i 是弧表达函数，它为每个弧分配一个表达式，例如：弧at y p e e ( a ) 】 = c q ) m s ，p 是与a 弧连接的位置。 9 i ：p - * e x p r q 5 是初始化函数，它给每个位置一个初始化表达式，例如：t y p e i ( p ) 】 = c q ) m s o 定义2 对一个c o l o rp e t r in e t s ，c p n = t , a ，s ，v , c ，g , e ，d ，我们定义如下概念： 1 一个标记是一个函数m ，它映射每一个位置p p 到一个多重集t o k e n s ，m ( p ) c ( p ) m s 。 2 初始化标记m o 定义为：m 0 ( p ) = i ( ) 对所有的p p 。初始化表达式没有自由 变量，所以是在空绑定( 用符号0 表示) 条件下进行初始化。 3 一个变迁的变量t 被表示为v a t ( 0 口v ，它由t 的防卫表达式中出现的自由变量和连 接到t 的弧表达式中的变量组成。 4 一个变迁的绑定是一个函数b ，它映射每个变量v v a t ( 0 为一个值b ( v ) t y p e v 。 5 。 基于属性的层次移动i p v 6 ( h m 口v 6 ) 协议的验证 一个变迁的所有绑定的集合表示为b ( t ) 。 5 一个绑定元素是一对( t ，b ) ，这里t t 并且b b ( t ) 。一个变迁t 的所有绑定元素 的集合b e ( t ) 定义为b e ( t ) = ( t ，b ) lb b ( t ) ) 。c p n 模型中所有绑定元素的集合用 b e 表示。 6 y b e m s 是一个绑定元素的非空有限多重集。 层次化c p n 的形式化定义： 定义3 层次化c p n 模型是四元组c p n h = ( s , s m ，p s ，f s ) 其中： 1 s 是模型的有限集合。每个模型都是c p n 的模块s = ( ( p 8 ，i s ，a s ，s8 ，v s ，c 8 ，g 8 ，e 8 ，d ，r s s i l b ，p s p o r t ，p t s ) 。要求( p 8 1ut s l ) n ( p 8 2ut 8 2 ) = 矽对于所有的s l ，8 2 s 并且s l s 2 。 2 s m ：t s l i b - s 是子模型函数，它为每个替代变迁分配二个子模块。并且要求模块层 次是非循环的。 3 p s 是端口凄接口关系函数，它对每一个替代变迁分配端口套接口的关系 p s ( t ) 口p 。o c k ( t ) 碟n 。对所有的( p ，p ) p s ( t ) 和所有的t t s i l b ，等式s t ( p ) = p t ( p ) ，c ( p ) - - - c ( p ) ，i ( p ) 0 = i ( ) ( ) 都成立。 4 f s 口2 p 是非空的融合集，这样对所有p ，p f s ，所有f s f s ，等式c ( p ) = c ( p 7 ) ，i ( p ) ( ) = i ( p ) ( ) 成立。 定义4 基本属性：对于一个给定系统，基本属性是该系统上，具有的最简单的行为、功能或 特性。 定义5 并发属性：对于一个给定系统，由多条c p n 基本属性构成的并发情况我们称之为并发 属性。 2 3c p n t o o l s 简介 本文使用丹麦奥胡斯大学开发的c p nt o o l s 5 】来对协议进行建模，分析和验证。c p n t o o l s 是一款集编辑，模拟，分析于一身的形式化建模工具。c p nt o o l s 工具可以用于c p n 模 型的编辑，模拟，状态空间分析，和性能分析等。并且c p nt o o l s 工具支持有时间和无时间 的层次c p nm o d e l s 。 c p nt o o l s 提供了良好的图形用户接口，它有一种回馈机制可以将错误进行定位，在 p e t r i 网建立的过程当中，它进行增量语法检查及代码生成，在一定程度上保证了模型的正确 6 7 基于属性的层次移动口v 6 ( h m 口v 6 ) 协议的验证 第3 章h m i p v 6 协议的模型建立 本章首先对h m i p v 6 协议进行了层次化抽象，并且抽象出每个模块的正确属性，然后对 抽象的模块进行层次化建模，最后共同组成了h m i p v 6 协议模型。 3 1c p n 模型的抽象 模型是现实的抽象；在建立协议模型时，要保证抽象的属性必须是安全的、正确的，并 且需要控制好抽象的程度，抽象粒度太细，会造成模型过于庞大而不便于分析；同样抽象力 度太粗则容易造成抽象出属性不完备，无法正确表现协议的功能。由于层次化建模可以清晰 的描述各个不同层次的功能，减少各个层次的规模，使得我们在进行验证时能更清晰的分析 模型属性，所以在设计模型时采用了层次化建模的方法 6 1 。图3 1 是h m i p v 6 协议的层次描 述以及各主要子模块的功能介绍。 t o p 敝 c h 删i i p 昭 家乡代理模块主要用于绑定m u 信息 逼信节点梗块，主要用于与肌n 信送数据 锚节点模块，用于绑定b u 肖息并返回 c 埒肖息- 处理隧道消息并转发 路由梗块，用于发i 差路由广播以及转发各 种数据 啊n 髓s e t 薯整薯亨缓装矗署委蓉鉴翳寡岳嚣南嘉晕进 图3 1h m i p v 6 协议抽象层次框架 f i g u r e3 1h m i p v 6a b s t r a c tl a y e rf r a m e 在抽象层次关系表中，抽象级别较低的模型作为抽象级别高一层的模型中的替代变迁的 实现。表格3 1 描述了每一抽象层次的功能，和底层的事件。 表格3 1h m i p v 6 抽象层次功能事件描述 t o p描述项层h m i p v 6 拓扑 h a 描述家乡代理的功能行为 接收识别m n 发送的绑定更新 更新m n 新的绑定信息 8 内蒙古大学硕士学位论文 转发c n 发送给m n 的数据包 c n 描述通信结点的功能行为 接收m n 发送的数据 向m n 发送数据 m n 描述移动结点的功能行为 接收并识别r a s 发送的路由广告信息 向m a p 发送m n 的绑定更新( r c o a ，l c o a ) 当发生“宏移动”后向h a 发送绑定更新 接收从m a p 返回的绑定更新确认 确认更新b u 后，m n 更新存储的( r c o a ，l c o a ) m n 通过隧道向c n 发送数据包 m n 通过隧道接收c n 发来的数据包 m a p 描述了移动锚点m a p 的功能行为 接收m n 的绑定更新 更新m a p 绑定表中m n 的绑定信息 返回绑定确认信息b u a c k 转发m n 向h a 发送的绑定更新包 向m n 或c n 转发数据消息 ， 接收来自m n 或c n 的数据消息 a r s 描述了接入路由的功能行为 向m n 发送路由广告 转发m a p 和m n 间的数据包 3 2 建模约束条件 众所周知，自然语言是具有二义性的，因此建模时首先要将自然语言描述的文档进行形 式化描述。同时为了能高效的分析协议，在建立h m i p v 6 协议模型时定义了一系列的约束条 件，使得模型在正确描述的前提下可以高效的进行分析。本文对h m i p v 6 协议的建模约束包 括如下几个方面： 建模中省略网络传输部分。 对于宏移动功能和微移动功能，由于单个m n 就可以覆盖，所以只考虑一个m n 结 点的情况。 对于m a p 和a r ，我们考虑到两个m a p 和三个a r 就能覆盖所有功能，因此分析时 9 基于属性的层次移动m v 6 ( h m i p v 6 ) 协议的验证 只考虑两个m a p 和三个a r 的情况。 本文在分析不同属性时，在保证能覆盖该属性的情况下，使用最少的节点进行模拟分 析。 ， 假设当一个m n 在一个a r 作用域时a r 的路由广告信息就已经知道该移动节点的到 来。 经过上述约束和抽象后h m i p v 6 协议的模型能更加清晰的描述协议属性，并且控制了模 型的规模，便于模型的验证和协议属性的分析。 3 3 数据建模 对于c p nt o o l s ，模型中t o k e n 必须属于某一指定的颜色集( c o l o rs e t ) 。c p nt o o l s 除了支 持u n i t ，1 n t ，b o o l ，s t r i n g 等基本c o l o r 集外，还可以根据使用者的需要进行扩展。图 3 2 给出了h m i p v 6 协议模型的主要数据类型的c o l o rs e t 的声明。 图3 2 数据类型 f i g u r e3 2d a t at y p e s 表格3 2 是对主要的报文和绑定记录数据类型说明： 表格3 2 数据类型描述 c o l s e tp r e = i n t ； 时序标记信息，用于并发情况下标记发包的顺 序，数字越大表示是越后发送的包 e o l s e tr a m s g = 路由广告信息，由r c o a ，l c o a ，m n 节点名字 p r o d u c tr c o a 幸l c o a m n p r e ； 和时序标记共同构成 c o l s e tb u m s g = 绑定更新信息，由r c o a ，l c o a ，m n 结点的名 p r o d u c tr c o a 幸l c o a * n o d e p i l e ； 字和时序标记共同构成 c o l s e th a s e t = 发送给家乡代理的绑定更新，由r c o a ，h a 名 p r o d u c tr c o a h a * n o d e p r e ； 字，m n 结点名字和时序标记共同构成 1 0 内蒙古大学硕士学位论文 c o l s e ta c k m s g = 绑定更新确认信息，由r c o a ，l c o a ，m n 节点 p r o d u c tr c o a 毒l c o a m n p r e ； 名字和时序标记共同构成 c o l s e td a t a m s g = 数据包，由源地址，目的地址以及数据共同构成 p r o d u c ts o u r c e 宰d e s d a t a ； c o l s e t 心d r a = m n 的绑定信息，由m n 所在的r c o a ，l c o a ， p r o d u c tr c o a 拳l c o a 幸m n 宰h a 奉p i l e ； 家乡代理，m n 节点名字和时序标记共同构成 c o l s e tm s g = u n i o nra m s g ：r am s g + 数据包中的交互报文，用u n i o n 类型同一组织， b u m s g ：b um s ( 计a c k m s g ：a c km s ( 计h a 共六种类型，每个数据包中的报文只能为六种中 b u m s g ：h a s e t + d a t a m s g ：d a t a _ m s g ； 的一种 c o l s e tp a c k e t = 数据包，由报文信息，发包的源地址s o u r c e ， p r o d u c tm s g 毫s o u r c e 枣d e s ； 目的结点d e s t i n a t i o n 共同构成 3 4c p n 层次化建模 下面介绍h m i p v 6 模型的主要设计及其功能。为了验证需求，可将库所定义为可观察库 一 所，下面图中的红色库所为定义的可观察库所。 3 4 1t o p 层建模 t o p 层的功能： 描述各结点m n 、a r s 、m a p 、h a 、c n 间的网络拓扑关系。 具体设计如图3 3 所示 h m i p v 6 协议模型t o p 层由五个模块构成：m n 、a r s 、m a p 、h a 、c n 。这五个模块 在图中都用替代变迁来表示，具体功能由各自的子页面具体实现。 图3 3 t o p 顶层模型 f i g u r e 3 3t o pl a y e rm o d e l t o p 层描述了各模块间相互的拓扑关系，通过t o p 层模型我们可以直观的看到相互通信 的模块，了解到数据传输的方式。下面是对各个子模块的建模。 基于属性的层次移动口v 6 ( h m 口v 6 ) 协议的验证 3 4 2h a 层建模 h a 层功能： 接收并更新m n 的h a b u 绑定信息；转发来自c n 的数据消息。 具体实现，如图3 4 所示： h a 家乡代理层模型主要包含的两个功能： 1 、当m n 移动到不同m a p 域时，发生宏移动，需要向h a 发送绑定更新，通知h a 自 己的新的r c o a 。当收到h a b u 时由变迁h a s e t 判断h a b u 与存在的绑定更新是否一致。 如果一致则不进行绑定更新，如果不一致则对没有绑定记录的进行绑定。若有旧的绑定信息 就需要删除旧的绑定将其更新为新的绑定信息。 考虑到绑定信息可能的并发情况，在h an a 存储信息和h a b u 更新消息中添加一个字 段( p i 也) ，用于记录更新的存储消息的先后顺序。在变迁h a s e t 上进行判断，当收到的h a b u 的时间顺序小与存储绑定更新消息时，绑定更新不变化；反之，则更新绑定更新。 2 、转发来自c n 的数据包。当h a 接收到来自c n 的数据包后，通过查找h a n a 中绑 定信息以获得移动节点所在的区域转交地址( r c o a ) ，并转发给相应的m a p 。 3 4 3c n 层建模 图3 4 家乡代理层模型 f i g u r e 3 4h al a y e r m o d e l c n 层功能： 接收m n 发送给c n 的数据包，向m n 发送数据包。 具体设计，如图3 5 所示： c n 模块主要包含两个功能： 1 、当通信节点c n 收到了来自m n 的数据消息后，通过变迁r e cd a r a 判断收到的消 1 2 内蒙古大学硕士学位论文 息是否发送给c n 。如果是则将数据信息存储，否则丢弃，并自动生成一个数据包返回给相应 的移动节点。 2 、如果通信节点c n 将要向m n 发送数据，却不知道m n 的区域转交地址r c o a ，则 通信节点c n 需要通过家乡代理h a 与移动节点m n 进行通信。通过变迁s e n d 给h a 发送数 据包进行转发。 3 4 4m a p 层建模 图3 5 通信节点层模型 f i g u r e3 5c ni a y c rm o d e l m a p 层主要功能： 1 m a p 接收m n 通过a r s 发送的绑定更新信息b u ，判断是否更新，并确定是否发送 绑定确认信息。 2 m a p 接收m n 通过a r s 发送给h a 的绑定更新信息，并转发给h