【摘 要】
：
由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根
【机 构】
：
苏州技师学院,苏州大学计算机科学与技术学院,重庆工商大学融智学院
论文部分内容阅读
由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
其他文献
现阶段越来越多的人通过社交网络结识新朋友,如何为用户快速准确推荐朋友是考量平台服务能力的重要指标。提出了一种基于索引树的在线网络朋友推荐方法,即基于网络结构局部特
以布尔函数的导数和自定义的e-导数为研究工具,研究了一类特定Hamming重量的H布尔函数的代数次数、代数免疫性、相关免疫性之间的关联问题。得出H布尔函数的组成部分e-导数的
单调性在经典粗糙集属性约简过程中发挥着重要的作用.然而,在一些泛化模型（如量化粗糙集模型）中该性质并不存在.针对该问题,提出了量化粗糙集模型中下近似单调约简的定义,并给
对有序XML文档树进行编码,不需要访问XML原始文件就能够实现对XML数据的管理,提高了XML管理系统的效率。针对查询提出的编码方案具有很高的查询性能,但更新效率很低。为提高
提出了一种改进的基于粒子群算法的优化布局算法（Improved Particle Swarm Optimization,IPSO）来替换原有的基于模拟退火（Simulated Annealing,SA）算法的优化布局算法,使其更加适
形式概念分析是知识获取的一种有效工具,已被广泛应用到各个领域。从序形式背景出发,首先利用优势关系作为标准尺度,将序形式背景转化成单值形式背景;其次利用原有单值背景的
随着基于位置的服务在人们日常生活中日益普及,个人的位置隐私正面临着严重的威胁。基于增量近邻查询思想,结合反映人口分布的路网环境,提出了一种新的位置隐私保护方法。该
为了更好地解决含有弱边界、灰度不均匀的图像在分割时出现的轮廓线错误移动而导致分割结果错误的问题,结合图像的统计信息,构造出一种新的符号压力(SPF)函数,提出了一种基于改进的压力符号函数的变分水平集图像分割算法。首先,利用新的压力符号函数代替边缘函数,构造了新的活动轮廓模型;其次,该算法保持了测地线活动轮廓(GAC)模型和chan-vese(C-V)模型的优点,使水平集函数演化到目标的边界上;最后
提出一种基于基站大功率信号广播的延迟容忍移动传感器网络消息路由机制(High-power Broadcasting based Routing scheme,HBR)。该机制使用两个通信频率f1和f2,基站以恒定大
无线体域网(Wireless Body Area Network,WBAN)不仅应用于医疗保健领域,而且在特殊人群监护、运动、娱乐以及军事等领域也有着巨大的应用价值,然而WBAN技术自身的特点将严重