（计算机科学与技术专业论文）基于color+petri+nets的hmipv6协议形式化验证研究.pdf

、-曩-_-，li ，+ 原创性声明 本人声明：所呈交的学位论文是本人在导师的指导下进行的研究工作及取得的研究成果。 除本文己经注明引用的内容外，论文中不包含其他人己经发表或撰写过的研究成果，也不包 含为获得内蒙古大学及其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对 本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。 学位论文作者签名：左丛 日期： 丛咝：笸：2 2 指导教师签名： 日期： 在学期间研究成果使用承诺书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：内蒙古大学有权将 学位论文的全部内容或部分保留并向国家有关机构、部门送交学位论文的复印件和磁盘，允 许编入有关数据库进行检索，也可以采用影印、缩印或其他复制手段保存、汇编学位论文。 为保护学院和导师的知识产权，作者在学期间取得的研究成果属于内蒙古大学。作者今后使 用涉及在学期间主要研究内容或研究成果，须征得内蒙古大学就读期间导师的同意；若用于 发表论文，版权单位必须署名为内蒙古大学方可投稿或公开发表。 日期： 星幺垒：冱! 以 日期： ； t t 内蒙占大学硕i j 学位论文 基于c olovp e t ri n e t s 的h p v 6 协议形式化验证研究 摘要 层次移动i p v 6 ( h i e r a c h i c a lm o b i l ei p v 6 ，h m i p v 6 ) 是在m i p v 6 ( 移动i p v 6 ) 的基础上针对m n ( 移动结点) 在小范围内快速移动所作出的一种改进技术。 h m i p v 6 针对m i p v 6 将全局性的大范围移动与一个区域内的小范围的移动都用 一种方式处理，对移动结点m n 在小范围内快速移动切换时更新报文频繁问题 提出了解决方法。h m i p v 6 对网络进行了层次化的划分，h m i p v 6 在每个区域内 引入了一个新的实体移动锚点( m a p ) ，使得移动结点的移动分为“宏移动 和“微移动两种情况，改进了最基本的m i p v 6 切换方案，减少了移动过程中 的丢包率和传输延时，提高了通信质量。 对h m i p v 6 进行形式化验证不仅可以给出协议的一种形式化的规范描述，并 且可以为后续协议改进提供了基础模型，便于协议改进的分析，并为软件的实 现提供了可信性保障。本文采用“基于事件 的分析方法对h m i p v 6 协议进行 属性提取，并采用了层次化方法和“通用模块”思想，构建了着色p e t r i 网( c o l o r p e t r in e t s ，c p n ) 的层次化模型，最后使用集成分析方法，采用了模拟执行、状 态空间报告、全状态空间分析、a s k c t l 模型检验确认模型满足协议要求。本 文中使用的c p n 采用图形语言和有效的形式化模型的组合，可以直观的模拟执 行，并且在描述复杂数据，层次化建模、并发、通信、同步中方面都有较强的 优势。 关键词：c p n ；微移动；宏移动；模型检测；形式验证 内蒙占大学硕_ i ：学位论文 i 、 内蒙古大学硕j 学位论文 h m i p v 6f o r m a lv e r i f i c a t l 0 nr e se 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 h i e r a r c h i c a lm o b i l ei p v 6 ( h m i p v 6 ) i sm a d et oi m p r o v et h em 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 nb a s e do nm i p v 6 ( m o b i l ei p v 6 ) h m i p v 6g i v e sa s o l u t i o nf o rm i p v 6d e a l i n gw i t ht h em o v e m e n ti nal a r g er a n g er e g i o na n dt h e m o v e m e n ti nas m a l lr a n g er e g i o nt h es a m es c h e m e ，b u tt h em nf a s tm o v i n gw i t h i na s m a l l r a n g er e g i o n w i l l b r i n gu p d a t ep a c k e t ss w i t c h i n gf r e q u e n t l y h m i p v 6 h i e r a r c h i c a l l yd i v i d e st h en e t w o r k h m i p v 6i n t r o d u c ean e we n t i t y m o b i l ea n c h o r p o i n t ( m a p ) i ne a c hr e g i o n ，m a p d i v i d e st h em o b i l en o d e sm o v e m e n ti n t o “m a c r o m o b i l i t y a n d “m i c r om o b i l i t y ”w h i c hi m p r o v e st h eb a s i c m i p v 6h a n d o v e rs c h e m e f o rr e d u c i n gp a c k e t sl o s sa n dt r a n s m i s s i o nd e l a yd u r i n gm o b i l i t ya n di m p r o v e st h e c o m m u n i c a t i o nq u a l i t y f o r m a lv e r i f i c a t i o nf o rt h eh m i p v 6p r o t o c o lc a nn o to n l yg i v e saf o r m a l s p e c i f i c a t i o nd e s c r i b e s ，p r o v i d e sab a s i sp r o t o c o lm o d e lf o rf o l l o w u pi m p r o v e m e n t ， f a c i l i t a t e st h ea n a l y s i so fi m p r o v i n gt h ep r o t o c o l ，a n dp r o v i d e sac r e d i b l eg u a r a n t e e f o rt h er e a l i z a t i o no ft h es o f t w a r e t h i st h e s i sa n a l y s e st h eh m i p v 6p r o t o c o l ，e x t r a c t s p r o p e r t i e s b a s e do ne v e n t s ；u s i n gh i e r a r c h i c a l m o d e l i n gm e t h o da n d u n i v e r s a l m o d u l e ”i d e a ，w eg i v eac p n ( c o l o rp e t r in e t s ) h i e r a r c h i c a lm o d e lo fh m i p v 6 p r o t o c 0 1 u s i n g t h e i n t e g r a t e dm e t h o d ，w ev e r i f y t h a tt h em o d e lf u l f i l lt h e r e q u i r e m e n t so fh m i p v 6p r o t o c o lb ys i m u l a t e de x e c u t i o n ，t h es t a t es p a c er e p o r t ，a l l s t a t es p a c ea n a l y s i s ，a s k c t lm o d e lc h e c k i n g t h ec p ni sc o m b i n a t i o no fa g r a p h i c a ll a n g u a g ea n de f f e c t i v ef o r m a lm o d e l c p ns i m u l a t e si n t u i t i v e l ya n dh a s s t r o n ga d v a n t a g e si nd e s c r i b i n gt h ec o m p l e xd a t a ，h i e r a r c h i c a lm o d e l i n g ，c o n c u r r e n c y , 内蒙占大学硕。l ：学位论文 c o m m u n i c a t i o n ，a n ds y n c h r o n i z a t i o n k e y w o r d s ：c p n ；m i c r om o b i l i t y ；m a c r om o b i l i t y ；m o d e lc h e c k i n g ；f o r m a l v e r i f i c a t i o n i v i 3 2 2 状态15 3 2 3 数据类型l5 3 2 4 协议属性描述15 3 3 本章小结1 6 第4 章模型建立17 4 1c p n 模型的抽象层次17 4 2 建模约束条件19 4 3 数据建模1 9 4 4 “通用模块”设计思想2 1 4 5c p n 层次化建模2 1 4 5 1t o p 层建模21 4 5 1 1h a 层建模2 3 4 5 1 2c n 层建模2 3 4 5 1 3m n 层建模2 4 4 5 1 3 1h a n d l er a 层建模：2 6 4 5 1 3 2h a n d l ed a t a 层建模2 7 4 5 1 4h m i p v 6 层建模2 8 4 5 1 4 1m a p 层建模2 8 4 5 1 4 2a r s 层建模3 0 4 6 本章小结3 l 第5 章模型的验证3 2 5 1 模型验证方法3 2 内蒙占大学硕二j ：学位论文 v i 弘粥甜钙如”钉铉钌 一 一 一 一 一 一 一 一 一 一 一 一 一 一 一 一 一 一 | 一 一 一 一 一 一 一 一 一一 | 一 一 一 一 证 一 一 一 证证 验 验验证况 元元验情 单单元发 一 能能单并一作功功能元结工动动功单小语步 移移道能章束结一 宏微隧功本结总进k 2 3 4 5 6 至1 2 ( 甘观钳”铂幛叭记致谢 第 参致 内蒙古大学硕。j j 学位沦文 图表目录 图2 1 h m i p v 6 基本架构5 图2 2 移动结点绑定更新过程序列图5 图2 3h m i p v 6 的隧道传输序列图一6 图2 4 牛产者消费者c p n 图例9 图3 1 c p n 的般设计方法1 2 图3 2 “基于事件”的设计方法1 2 表3 1 事件属性一1 4 表3 2h m i p v 6 协议属性16 图4 1h m i p v 6 协议抽象层次框架17 表4 1h m i p v 6 抽象层次功能事件描述18 图4 2 数据类型2 0 表4 2 数据类型描述2 0 图4 3h m i p v 6 顶层模型2 2 图4 4 家乡代理层模型2 3 图4 5 通信结点层模型2 4 图4 6 移动结点层模理2 5 图4 7 移动结点绑定更新处理层模型2 6 图4 8 移动结点处理接收隧道数据层模型2 7 图4 9 移动i p v 6 层次层模型2 8 图4 1 0 移动锚点层建模2 9 图4 1 1 接入路由层建模3 1 图5 1a r s 发送a r l 路由广告3 3 图5 2 发送绑定信息并暂存r a 3 4 图5 3 更新并发送确认信息a c k 3 4 图5 4m n 确认绑定信息3 4 图5 5m n 向h a 发送绑定3 5 图5 6h a 成功绑定m n 信息3 5 表5 1 宏移动状态报告3 6 图5 7 宏移动完全状态空间3 6 图5 8 宏移动变迁点火序列3 7 图5 9a s k c t l 检测宏移动绑定一致性3 7 图5 10m n 收到r a 2 后发送b u 并暂存r a 3 8 图5 1 1m a p 更新绑定并发送a c k 3 9 图5 1 2m n 更新绑定3 9 表5 2 微移动状态空间报告4 0 图5 1 3 微移动完全状态空间4 0 图5 1 4 微移动变迁点火序列4 1 图5 15a s k c t l 检验微移动绑定一致性4 1 图5 1 6m n 向c n 发送“h e l l o ”4 2 图5 1 7c n 收到m n 的数据并自动回复4 2 图5 1 8m n 收到c n 数据4 2 v i i 内蒙古大学硕j ：学位论文 5 3 隧道传输状态空间报告4 3 5 1 9 隧道传输完全状态空间图4 3 5 2 0 隧道传输点火序列。4 4 5 21a s k c t l 检验隧道传输4 4 5 4 并发情况状态报告1 4 5 5 5 死结点绑定情况1 4 5 5 2 2 模型改动1 一4 6 5 2 3 模型改动一2 4 6 5 2 4a s k c t l 检测模型并发4 7 5 - 6 死结点绑定情况2 4 7 5 2 5m n 移动到a r 2 内4 8 5 2 6m n 绑定( a r l ) 先发后至j 4 8 5 2 7 增加绑定序列号4 9 5 7 并发情况状态报告2 4 9 5 8 死结点绑定情况3 4 9 5 2 8a s k c t l 检测并发绑定结果5 0 v i i i 表图图图表表图图图表图图图表表图 内蒙。大学硕 = 学位论文 1 1 研究背景 第1 章引言 随着_ 百连网络的飞速发展和便携式移动终端的不断涌现，用广希望通过个人终端随时随 地的加入到互联网中，方便快捷地获取自己所需的信息。下一代互联网协议i p v 6 采用1 2 8 b i t 的i p 地址，彻底解决了i p v 4 地址不足的问题。为了支持瓦联网上的移动设备，并使其保留 不变的永久i p 地址，i e t f 在2 0 0 4 年公布了移动i p v 6 的标准r f c 3 7 7 5 。m i p v 6 1 】是一种在全 球瓦联网上提供移动功能的方案，具有可扩展性、可靠性和安全性的特点，并可以使结点在 链路切换时仍可保持正在进行的通信。m i p v 6 工作于网络层，可以在不同的链路层上使用， 同时对网络层以上也是透明的，不仪适用于同种介质网络间的移动，也适用于异种介质网络 间的移动，所以有广阔的应用前景。对于无线局域网而言，m i p v 6 主要解决全球范围内“宏 移动”管理的问题，而没有有限范围内的“微移动”管理问题，m i p v 6 没有区分“宏移动 和“微移动”，它将全局性的大范围移动与一个区域内的小范围的移动都用一种方式处理，这 样没有体现出网络的可扩展性和伸缩性。当移动结点快速移动时，由于移动结点需要在家乡 代理和通信结点之间传递大量的绑定更新报文，而它们可能相距较远，因此会产生严重的丢 包和延时等问题。 为了更好的处理移动结点m n 在小范围内快速移动切换时更新报文频繁问题，引入了 h m i p v 6 心1 ，h m i p v 6 在m i p v 6 的基础上，在每个区域内引入了一个新的实体移动锚点 ( m a p ) ，利用现有网络的层次结构，将网络进行了区域化的划分，这样将移动结点的移动区 分为“宏移动和“微移动”。当m n 在域内移动时，只向m a p 发送绑定更新，更新信息不 会发送到m a p 外部，h m i p v 6 可以大大减少绑定更新报文，从而提高网络传输数据的效率， 同时可以实现域内的快速切换。 1 2 国内外研究现状 2 0 0 3 年肩动的中国下一代互联网示范工程( c n g i 项目) 是国家级的战略项目，由八部委联 合发起并经国务院批准肩动，该项目的丰要目的是搭建下一代互联网的试验平台，i p v 6 是其 中要采用的一项重要技术，标志着我国i p v 6 商用化进程进入了实质性发展阶段。i p v 6 对下一 基十c o l o rp e t f in e t s 的h m i p v 6 协议形式化验证研究 代网络和3 g 网络的影响巨大。i e t f 一直负责i p v 6 标准主体部分的制定。2 0 0 4 年i e t f 公布 m i p v 61 办议r f c 3 7 7 5 后，为了改进小范围内移动结点性能问题于2 0 0 5 年8 月i e t f 制定了 h m i p v 6 的第一版标准r f c 4 1 4 0 。2 0 0 8 年1 0 月在前版的基础上i e t f 又制订了第二版 r f c 5 3 8 0 ，在新版中去掉了r f c 4 1 4 0 中动态m a p 发现可扩展性部分。h m i p v 6 的提出是为 了解决m i p v 6 小范围内的移动问题，所以围内外大多都着眼于研究及提出改进h m i p v 6 的切 换技术，使移动结点减少更新绑定的时间。比如对移动结点“微移动 无缝切换提出改进方 梨3 】【4 】，或对“宏移动”提出绑定优化方法减少切换延迟 5 】、或基于具体无线网络给出快速切 换方法【6 以及对绑定信息失效性的研究7 1 。对协议进行测试则较少：爱立信公司对r f c 4 1 4 0 开发了包括两个测试例的测试套，并对两个版本的h m i p v 6 实现进行了测试，没有发现重大 问题。而对h m i p v 6 协议进行形式化建模，验证研究方面的文章则鲜有公布。 协议验证最早出现于2 0 世纪8 0 年代。i b m ，n o r t e l ，i n t e l ，m o t o r o l a 等，都成立了自己 的验证小组，还有一些围际化的组织，如官方的i e t f ，i t u u 及成立于1 9 6 0 年非官方的i f i p ， 都推动了证验技术的理论发展。一年一度的国际会议v e r i f y 以及f o r t e 等，也极大地促 进了验证技术在计算机各个领域的应用。 目前i e t f 制定的i n t e m e t 协议标准r f c 仍使用自然语言描述。随着网络的飞速发展及对 服务性要求的提高，网络系统越来越复杂，只依靠传统软件工程方法不能设计出高质量的协 议。协议实现后再纠正协议描述中的错误代价高昂。形式化方法是传统的软件工程方法的重 要补充，它可以提高自动化的程度和更高的可靠性。形式化方法的主要内容包括两个方面： 形式化规约，形式化验证。形式化规约有多种方式：逻辑、自动机、p e t r i 、进程代数等。形 式化验证则包括定理证明、模型检测。用于建立形式化模型的方法虽然有很多，有限自动机、 s d l 、l o t o s ，但着色p e t r i 网( c o l o r e dp e t r in e t s ，c p n ) 适合对复杂通信和具有高并发行为 的系统进行建模与分析，在描述复杂数据、系统层次化建模、模型动态行为分析等方面具有 较强优势。与有限状态机( f i n i t es t a t em a c h i n e ) 相比，c p n 可以更为准确的描述和分析协议行 为的并发特性，而且c p n 的动态执行能力可以展示非常直观、实时的模型运行状态，便于模 型确认和改进。 对h m i p v 6 协议进行建模验证不仅可以给出协议的形式化协议规范描述，为后续协议改 进提供了基础模型，便于协议改进的分析，而且为协议软件的开发提供可信性保障。 1 3 研究内容和主要工作 本文主要使用c p n 对h m i p v 6 ( r f c 5 3 8 0 ) 进行建模，然后使用检验模型的方法对协议 内蒙占大学硕l 学位论文 进行验证。 本文的丰要工作和贡献包括下面几个方面： 本文对h m i p v 6 ( r f c 5 3 8 0 ) 采用了“基于事件”的语法分析方法提取协议系统属性。 首先从协议中先提取事件及事件的相巨关系再从事件出发寻找事件相关的输入、输 出、数据结构、状态和系统属性并逐步完善。并用时序逻辑的形式化方法描述协议属 性。 采用了层次化方法和“通用模块”思想，使用c p nt o o l s 对协议进行建模。采用层 次化的方法可以有效控制每层模型的复杂度，使模型清晰。给出的h m i p v 6 协议的 c p n 层次模型直观、准确的描述了协议。“通用模块 思想的采用可以方便快速的复 用各m n 、h a 、c n 、h m i p 结点，使模型可以快速添加上述结点构建更复杂的场景， 为研究协议复杂情况下的运行提供了可能。 以c p n 模型为基础对协议进行了验证。验证过程使用集成分析方法，对模型采用了 模拟执行、状态空间报告、全状态空间和a s k c t l 检测方法分析了h m i p v 6 协议的 正确性，并且验证了模型满足协议要求。在验证过程中发现了模型的不足并进行了相 应修改，经过验证正确，进一步完善了模型。 1 4 论文结构 本文结构如下：引言部分阐述了选题依据，和本文的丰要工作；第一章对h m i p v 6 协议对 m i p v 6 的改进方面进行了介绍，阐述了h m i p v 6 在小范围内处理m n 快速移动的原理和其快 速、平滑切换的优势；并对c p n 的直观性和描述并发的优势以及本文使用的c p nt o o l s 进行 了简要介绍；第二章对h m i p v 6 协议采用“基于事件”的语法分析方法抽取协议属性。先找 出事件的属性然后扩展寻找事件相关的数据结构等属性并逐步完善，最后用时序逻辑的形式 化的方法描述协议属性；第三章采用了“通用模块”思想对协议进行了层次化建模，给出了 h m i p v 6 协议的c p n 层次化模型，很好的控制了每层的规模，并清晰的描述了协议每个抽象 层次的功能；第四章采用集成分析方法对协议进行了验证。首先对协议进行了基本功能单元 的划分，用模拟执行、状态空间分析、a s k c t l 检验等方法对每个单元进行验证。在单元验 证正确的情况下，进一步对单元的并发情况进行验证；第五章对本文工作进行了总结，并提 出了本文的一些不足之处，在今后的工作中需逐步完善。 基于c o l o rp e t r in e t s 的h m i p v 6 协议形式化验证研究 第2 章背景知识 本章对相关的背景知识进行了简要介缁。对h m i p v 6 协议的基本架构和各实体间绑定更 新收发报文序列及隧道传输序列简要说明，并对本文丰要使用的c p n 和c p nt o o l s 进行了介 绍。 2 1h p v 6 协议简介 m i p v 6 是为了解决结点跨越不同网段移动而设计的，m i p v 6 协议允许移动结点在网络拓 扑内移动的同时保持和通信结点的连接，但每次移动时必须向家乡代理h a 发送绑定更新 b u 。移动结点m n 可以在发送绑定更新b u 后，通过家乡代理h a 立即发送数据包，但家乡 代理h a 直到收到绑定更新b u 后才会把数据包正确发送到m n ，这个过程就引起了至少半 个往返的延迟。如果移动结点m n 要等待绑定确认b a ，则会增加更多的延迟。当移动结点 在小范围内快速移动时，由于移动结点需要在家乡代理和通信结点之间传递大量的绑定更新 报文，当移动结点m n 和其家乡代理h a 距离很远，在世界的不同地方时，往返时间则会相 对更长，加上连接层、i p 层的延迟，就会影响到上层协议。 而且在无线环境中，更新位置的信号会导致连接中断，数据包丢失和延时等问题，如果 减少了发送给通信结点c n 和家乡代理h a 的信息数量，将使m i p v 6 的外网从中受益。如果 减少了时间紧迫的切换期间的这些延迟将会提高m i p v 6 的性能。 h m i p v 6 是在m i p v 6 协议基础上提出的，针对于m i p v 6 的移动结点m n 在小范围内快 速移动切换时更新报文频繁，丢包率高的问题提出了解决方法。h m i p v 6 在每个区域内引入 了一个新的实体移动锚点( m a p ) ，改进了最基本的移动i p 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 ) ，通过r c o a 和l c o a 即可找到移动结点，这两个地址在宏观移动和微观移动中非 常有用。“宏移动”和“微移动 逻辑结构图如图2 1 所示。当m n 从a r l 处移动到a r 2 处的时候，为“微移动”，由m a p l 充当本地的家乡代理，此时m n 的绑定更新只有l c o a 改变，绑定过程只需要在a r l 、a r 2 、m a p l 、m n 之间进行，并且绑定更新过程完全对h a 和c n 透明；而当m n 继续从a r 2 移动到a r 3 的时候，因为a r 3 隶属于m a p 2 ，为“宏移 4 内蒙t f 。大学硕+ 1 ：- 7 - 位论文 动”，绑定更新r c o a 、l c o a 都改变，此时绑定更新过程和移动i p v 6 一样，需要h a 、c n 的参与。 m n 图2 1 h m i p 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 各实体绑定更新期间收发报文的序列图如图2 2 所示： 田曰臣町 图2 2 移动结点绑定更新过程序列图 f i g u r e2 2m nu p d a t eb u sp r o c e d u r eo r d e r 各阶段的具体含义如下： 1 ) 当m n 移动到a r 作用域后，会收到a r 发送的路由广告r a ，r a 中包含绑定更新所 需要的信息。 2 ) m n 取得绑定信息( r c o a ，l c o a ) 后通过a r 向m a p 发送绑定更新b u 。 3 ) m a p 对m n 的绑定信息进行注册更新，并返回绑定确认a c k 。 基于c o l o rp e t r in e t s 的h m i p v 6 协议形式化验诅：研究 4 ) m n 收到a c k 后，如果与暂存的绑定信息( r c o a ，l c o a ) 匹配就可将绑定存储。 这时如果原绑定信息的r c o a 和新绑定信息的r c o a 相同，则发生的是“微移动”，1 4 步就完成了“微移动”的结点注册绑定更新；如果不同，说明发牛了“宏移动”，还需要： 5 ) 向h a 发送绑定更新。 6 ) h a 对m n 的绑定更新并存储。 1 6 步完成“宏移动”的结点注册绑定更新。 成功注册后m a p 与m n 之间建立双向隧道。发牛“微移动”对c n 来说是透明的，原因 就在于m n 与m a p 间的双向隧道。m n 向c n 发送的所有包都通过隧道t u n n e l 到m a p ，包 的外部l c o a 为源地址，m a p 为目的地址；包的内部m n 的r c o a 为源地址，通信结点为目 的地址。而发送给m n 的目的为r c o a 的包都将被m a p 截下来，利用t u n n e l 发给m n 。c n 只知道m n 的r c o a ，m a p 负责将包发送到正确l c o a ，所以发牛“微移动”时m n 对c n 来说是透明的。图2 3 为隧道传输的序列图。 田固田田 氐 j 隧道 jd a t a t o c n 、 d a t a t o c n d a t ag oc n d a t at om n -to_mnlip i ， 氐 - - - - 进入隧道 图2 3h m i p v 6 的隧道传输序列图 f i g u r e2 3h m i p v 6t u n n e lt r a n s i t i o no r d e r 综合以上h m i p v 6 有以下两个明显的改进： 1 用分级的思想区别小区域移动与大区域移动是非常适合互连网的。它提高了切换性 能，因为小区域切换被限制在了一个很小的网络范围内，这样： a ) 它可以减小切换过程中的延时，加快切换的速度，即快速切换，使通信更加 流畅。 b ) 它减少了切换时的丢包率，即平滑切换。增强了通信的连续性。 2 在一个域内的移动，它的切换信令不会传送到整个网络中去。明显的减少了网络中 的切换管理信令，避免了网络中的信息拥塞。 6 内蒙占大学硕l ：学位论文 2 2g p n 和c p n t 0 0 l s 简介 c p n 8 】 9 】是一种图形语言，其在建模和验证并发、分布式系统和其它系统的方面有较强 优势，扮演着重要角色。c p n 是离散行为模型语言并结合了高层程序语言的能力，它提供了 基础的图形表示和模型并发、通信、同步的能力。c p n 的m l ( m a r k u pl a n g u a g e ) 程序语言 基于标准的m l 程序语言，它提供了基木的数据类型定义( 通过p r o d u c t ，u n i o n 等可以组合 表示复杂数据类型) ，数据操纵的描述，可以创建出紧凑的和参数化的模型。c p n 的模型语 言是通用目的的建模语言，它并不只适用于一类系统而是面向广泛的系统并可以描述并发系 统。它的典型的应用领域包括通信协议、数据网络、分布式算法、嵌入式系统，在工业领域 也有很多应用。 这里先给出c p n 和层次化c p n 的形式化定义，稍后将给出一个具体的例子对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 ，ge ，i ) ，其中： 1 p 是一个有限位置( p l a c e ) 的集合。 2 t 是一个有限变迁的集合，t 满足p n t = 矽。 3 a p x tutx p 是有向弧的集合。 4 s 是有限非空c o l o rs e t 类型的集合。 5 v 是有限变量的集合，对所有变量v v 满足t y p e v 】。 6 c ：p 一是c o l o u rs e t 函数，它给每个位置分配一个ac o l o u rs e t 。 7 g ：t - * e x p r v 是防卫表达式，每个变迁有一个防卫表达式，n o n ：t y p e g ( t ) 】= b o o l 。 8 e ：a e x p r v 是弧表达函数，它为每个弧分配一个表达式，例如：弧at y p e e ( a ) = c ( p ) m s ，p 是与a 弧连接的位置。 9 i ：p e x p r 西是初始化函数，它给每个位置一个初始化表达式，例如：t y p e i ( p ) = c ( p ) m s 。 定义2 对一个c o l o rp e t r in e t s ，c p n = ( p , t , a ，s ，v , c ，g , e ，i ) ，我们定义如下概念： 1 一个标记是一个函数m ，它映射每一个位置p p 到一个多重集t o k e n s ，m ( p ) c ( p ) m s 。 2 初始化标记m o 定义为：m o ( p ) = i ( p ) ( ) 对所有的p p 。初始化表达式没有自由 变量，所以是在空绑定( 用符号( ) 表示) 条件下计算初始化。 基于c o l o rp e t r in e t s 的h m i p v 6 协议形式化验b e 研究 3 一个变迁的变量t 被表示为v a r ( t ) v ，它由t 的防卫表达式中出现的自由变量和 连接到t 的弧表达式中的变量组成。 4 一个变迁的绑定是一个函数b ，它映射每个变量v v a r ( t ) 为一个值b ( v ) t y p e v 。一个变迁的所有绑定的集合表示为b ( t ) 。 5 一个绑定元素是一对( t ，b ) ，这里t t 并且b b ( t ) 。一个变迁t 的所有绑定元 素的集合b e ( t ) 定义为b e ( t ) = ( t ，b ) fb 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 ，t 8 ，a 8 ，s8 ，v 8 ，c 5 ，g 5 ，e 8 ，1 5 ) ，t s s u b , p s p o n , p t 8 ) 。要求( p 5 1 ut 8 1 ) n ( p 5 2u t 5 2 ) = 对于所有的s l ，s 2 s 并且s l s 2 。 2 s m ：t 。b s 是子模型函数，它为每个替代变迁分配一个子模块。并且要求模块层 次是非循环的。 3 p s 是端口套接口关系函数，它对每一个替代变迁分配端口套接口的关系 p s ( t ) p s o c k ( t ) 碟“。对所有的( p ，p ) p s ( t ) 和所有的t t s u b ，等式 s t ( p ) = p t ( p ) ，c ( p ) = c ( p 7 ) ，i ( p ) ( ) = i ( p ) ( ) 都成立。 4 f s 2 p 是非空的融合集，这样对所有p ，p f s ，所有f s f s ，等式c ( p ) = c ( p ) ，i ( p ) 0 = i ( p ) ( ) 成立。 下面给出一个生产者消费者问题的例子，对c p n 及层次c p n 中的一些基木概念做出 解释，如图2 4 所示。 图中的生产者生产三种水果：a p p l e ，b a n a n a ，o r a n g e ，生产出后放到b u f ( 盘子) 中， 然后消费者从b u f 中取出，吃掉水果。 图2 4 的1 部分为牛产者消费者的c p n 图。椭圆形的表示位置，矩形的表示变迁。在c p n 中位置可以被定义为多种基本或复杂数据类型，a 位置右下角的f r u i t 标记出a 的数据类型。 现在a 位置有标记( m a r k i n g ) a p p l e 和b a n a n a ( 表示两个水果) ，可以通过变迁p r o d u c e 点火( 生产) ，点火后a 的一个标记转移到b ( 表示生产出一个水果) ，经s e n d 变迁发送到 b u f ，现在b u f 中有一个标记o r a n g e ( 表示盘子中有一个o r a n g e ) ，等待消费者取走，消费。 内蒙古大学硕j ：学位论文 由于c p n 图的直观性和动态可执行性，可以很好的描述和展示生产者消费者问题。 缪q f r u 露i tq r 0 ”“ 由佃申钾 鬲。u 接 ，、jj 、 r 苣一自 l 图2 4 生产者消费者c p n 图例 f i g u