【摘 要】
：
随着互联网的高速发展,网络协议标准也不断地更新和完善。如何更有效地提高网络服务,已成为网络协议工程领域的关键问题之一。层次移动IPv6协议作为移动IPv6协议的扩展,在移
论文部分内容阅读
随着互联网的高速发展,网络协议标准也不断地更新和完善。如何更有效地提高网络服务,已成为网络协议工程领域的关键问题之一。层次移动IPv6协议作为移动IPv6协议的扩展,在移动IPv6的基础上对移动节点在小范围内快速切换作出了改进。CPN (Coloured Petri Nets)是一种形式化建模语言,适用于通信和并发系统。CPN为使用者提供了直观的图形化的形式化描述方法,并且CPN的模型语言是通用目的的建模语言。本文通过形式化方法对自然语言描述的HMIPv6 (RFC5380)协议规范进行建模,并对HMIPv6协议的基本属性进行形式化验证。由于协议并发行为引发的状态爆炸问题严重影响了验证工作的进行,本文提出了模型化简和抽象的方法,化简法将模型化检为多个并发子模型,抽象法将并发子模型进行抽象层次的提升,合并一些库所和变迁,以减少状态空间规模,保证属性验证工作的效果。最后,本文将以上方法应用于HMIPv6协议模型,验证了方法的有效性。
其他文献
汉语基本块识别是汉语语块分析体系中的基础任务之一,属于浅层句法分析的一个环节。对给定的汉语句子,汉语基本块识别任务将形式化为以字为基本标注单位的序列标注问题。基于
零形式是指句子中隐式的、未显示表达的语义成分,是传统语义角色标注不能标注出的语义角色,也不是谓词依存成分的语义角色。零形式被区分为有定的零形式和无定的零形式,其中,
云计算作为新兴的一种计算模式，它以互联网为基础，以服务的方式对外提供计算能力。它将网络上的各种资源整合成一个分布式服务集群系统，为用户提供可以缩减或扩展的计算资源。计
随着信息社会的不断发展,人们对信息的需求量逐渐增多,Web上拥有大量的信息资源,它逐渐成人们获取信息的重要途径。然而,由于不同的网站使用的数据往往具有不同的数据格式,所
随着信息化迅速推广和普及,导致各行各业基础信息量成几何倍增。海量存储和大并发成为主流大型数据库的标记。同时异地、跨行业的数据库服务器之间的数据信息交换、交互的诉
随着信息技术的迅猛发展,在网络监控、电信数据管理和金融服务等领域源源不断地产生新数据。具有海量、连续、多变及潜在无限性等特征的数据流不仅为数据存储带来挑战,也加大
稀疏矩阵向量乘(SMVM)运算是许多工程计算与科学计算的核心,近年来随着FPGA的广泛应用,基于FPGA平台的SMVM运算研究工作也在不断地深入。针对FPGA特有的并行性,研究者们提出
Internet的开放性和共享性环境给人们带来了便利,网上购物逐渐深入人们的生活,由此,电子商务得到飞速的发展。但是,近年来电子商务的发展频繁受到各种安全隐患和不诚信因素的
微数据是指与个体相关的数据,如人口统计数据、客户购物数据、患者医疗数据等,这些数据在趋势分析、市场预测等应用中具有重要的价值。但是如果直接发布或共享微数据会泄漏大
随着软件规模的逐渐增大,软件测试在整个软件开发过程中占有非常重要的地位,是保证软件质量、提高软件可靠性的关键。随着Internet的迅猛发展,分布式系统大量涌现。新一代电