一种针对CP-nets并发模型的验证方法
本文关键词:一种针对CP-nets并发模型的验证方法
【摘要】:状态爆炸问题导致CP-nets并发模型的正确性验证工作十分困难。提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正。这在一定程度上避免了状态爆炸问题并实现了模型验证。通过将上述方法应用于HMIPv6协议模型,验证了其有效性。
【作者单位】: 内蒙古大学计算机学院;
【关键词】: 模型验证 化简 抽象 状态爆炸
【基金】:国家自然科学基金资助项目(61262017);国家自然科学基金资助项目(61163011) 内蒙古自然科学基金资助项目(2012MS0922);内蒙古自然科学基金资助项目(2011MS0912)资助
【分类号】:TP393.04
【正文快照】: 1引言在现实世界中,并发系统是无处不在、不可或缺的;在计算机软件领域中,随着互联网的日益发展,并发软件也成为了最为主流的软件形式之一。例如,包括移动网络协议在内的各种网络协议、包括云计算软件在内的各类网络软件都具有并发性特点。并发系统已成为研究热点之一,例如,关
【参考文献】
中国期刊全文数据库 前3条
1 孙涛;叶新铭;刘靖;杨蒙;;一种基于CPN的协议测试序列生成方法[J];解放军理工大学学报(自然科学版);2012年02期
2 颜炯;王戟;陈火旺;;基于模型的软件测试综述[J];计算机科学;2004年02期
3 曾一;张利武;张元平;袁纲;李强;;一种基于活动图的并发软件测试线索生成方法[J];计算机科学;2007年12期
【共引文献】
中国期刊全文数据库 前10条
1 陈闯;;基于UML的网站设计与实现——以毕节学院人事处网站为例[J];毕节学院学报;2009年04期
2 陈颖慧;邱雪松;刘益畅;唐凡;高志鹏;;基于模型的Web Service性能测试方法[J];北京邮电大学学报;2009年S1期
3 田志民;林奇;罗雪莱;孟庆浩;;一种面向国防工业的应用软件漏洞检测方法[J];保密科学技术;2012年01期
4 牟小玲;丁晓明;张望;;基于Petri网的测试用例生成研究进展[J];重庆交通大学学报(自然科学版);2012年01期
5 雷航;马成功;;Markov模型的软件可靠性测试充分性问题的研究[J];电子科技大学学报;2010年01期
6 严海军;;基于UML的江苏省药物研究所网站分析设计[J];电脑知识与技术;2011年35期
7 杨广华;齐璇;施寅生;;基于威胁模型的软件安全性测试[J];计算机安全;2010年02期
8 吕金和;;由指针和数组带来的软件安全性缺陷[J];计算机安全;2010年05期
9 吕金和;;软件安全性测试研究[J];计算机安全;2010年08期
10 郑薇玮;;基于模型的软件测试新工具——UPPAAL TRON[J];福建广播电视大学学报;2010年06期
中国重要会议论文全文数据库 前5条
1 冯亚冬;熊波;;基于适航认证的FADEC软件自动化测试平台的研究[A];2011航空试验测试技术学术交流会论文集[C];2010年
2 陈振华;王峰;;操作剖面与软件可靠性[A];2006年全国理论计算机科学学术年会论文集[C];2006年
3 杨春晖;李冬;熊婧;;一种基于任务模块的实时软件可靠性评价模型[A];2010第十五届可靠性学术年会论文集[C];2010年
4 陈颖慧;邱雪松;刘益畅;唐凡;高志鹏;;基于模型的Web Service性能测试方法[A];中国通信学会通信软件技术委员会2009年学术会议论文集[C];2009年
5 孙晶;赵会群;马云峰;;基于TTCN的手机游戏软件测试方法研究[A];第四届中国测试学术会议论文集[C];2006年
中国博士学位论文全文数据库 前7条
1 刘振宇;服务网格环境中场景测试的关键技术研究[D];复旦大学;2010年
2 曾凡平;软件漏洞测试若干问题研究[D];中国科学技术大学;2009年
3 钱思佑;图形用户界面测试中相关问题研究[D];中国科学技术大学;2010年
4 张毅坤;COTS构件集成软件系统的测试方法研究[D];西安理工大学;2008年
5 李丽;航天相机主控软件测试用例自动生成技术的研究[D];中国科学院研究生院(长春光学精密机械与物理研究所);2010年
6 丁晓明;基于构件的软件开发关键问题研究[D];西南大学;2012年
7 孙涛;基于CP-nets模型的并行软件测试方法研究[D];内蒙古大学;2012年
中国硕士学位论文全文数据库 前10条
1 张作梅;教育软件自动测试系统设计[D];华东师范大学;2010年
2 靖焱林;基于UML-XML的车载设备测试用例生成方法研究和实现[D];北京交通大学;2011年
3 劳阳辉;AOP代码中几种特定缺陷的软件测试方法[D];昆明理工大学;2010年
4 黄X;软件缺陷分析及质量度量系统的设计与实现[D];西安电子科技大学;2011年
5 王新红;构件软件黑盒测试研究及应用[D];华北电力大学;2011年
6 郭丽娟;基于即时验证的嵌入式软件验证技术研究[D];南京航空航天大学;2010年
7 冯亚冬;适航认证的FADEC软件自动测试平台的研究[D];上海交通大学;2011年
8 姜喜梅;基于马尔可夫链的单证关系建模的研究与实现[D];哈尔滨工程大学;2011年
9 宋建斌;城市轨道交通运营管理系统测试与评价方法研究[D];苏州大学;2011年
10 李伟;呼叫中心系统性能测试和分析[D];北京邮电大学;2012年
【二级参考文献】
中国期刊全文数据库 前4条
1 颜炯;王戟;陈火旺;;基于模型的软件测试综述[J];计算机科学;2004年02期
2 梅宏;王千祥;张路;王戟;;软件分析技术进展[J];计算机学报;2009年09期
3 顾庆,陈道蓄,谢立,韩杰,孙钟秀;基于有限状态进程的事件约束定义[J];软件学报;2002年11期
4 赵炜;曾一;张利武;;基于UML活动图生成功能测试线索[J];计算机工程与设计;2006年22期
中国硕士学位论文全文数据库 前1条
1 赵炜;基于UML提取系统测试线索方法的研究[D];重庆大学;2006年
【相似文献】
中国期刊全文数据库 前10条
1 吴昌;肖美华;罗敏;刘俏威;熊昊;;安全协议验证模型的高效自动生成[J];计算机工程与应用;2010年02期
2 苏继斌;肖宗水;肖迎杰;;网络风险评估渗透图生成算法的设计[J];计算机工程与应用;2010年17期
3 苘大鹏;周渊;杨武;杨永田;;用于评估网络整体安全性的攻击图生成方法[J];通信学报;2009年03期
4 苏继斌;肖宗水;肖迎杰;;基于渗透图的网络弱点分析与研究[J];计算机工程;2009年23期
5 陈国彬;任强;张广泉;;一种基于抽象与精化技术的Web服务组合验证方法[J];计算机工程与科学;2011年09期
6 刘培,周明天;基于串空间的认证协议分析[J];实验科学与技术;2005年03期
7 王之梁;吴建平;尹霞;施新刚;;基于MSC测试目的的协议互操作性测试生成[J];北京邮电大学学报;2006年S1期
8 苘大鹏;张冰;周渊;杨武;杨永田;;一种深度优先的攻击图生成方法[J];吉林大学学报(工学版);2009年02期
9 舒挺;孙守迁;王海宁;徐伟强;李文书;;启发式探索的协议测试序列生成[J];北京邮电大学学报;2009年06期
10 杜彦华;范玉顺;李喜彤;;基于模块化可达图的服务组合验证及BPEL代码生成[J];软件学报;2010年08期
中国重要会议论文全文数据库 前2条
1 谢朝海;陶然;李志勇;李继勇;;基于弱点相关性的网络安全性分析方法[A];全国网络与信息安全技术研讨会论文集(上册)[C];2007年
2 逄建;张广胜;于朝萍;;基于Petri网的网络系统脆弱性评估[A];第十九次全国计算机安全学术交流会论文集[C];2004年
中国博士学位论文全文数据库 前3条
1 王玉英;基于赋时有色Petri网的Web服务组合建模验证与测试技术研究[D];西安电子科技大学;2012年
2 杨学红;BPEL流程的故障模式及其静态分析技术的研究[D];北京邮电大学;2011年
3 李华;基于属性的网络协议建模与互操作性测试方法研究[D];内蒙古大学;2010年
中国硕士学位论文全文数据库 前10条
1 刘鹏;面向存储的正则表达式匹配算法研究[D];解放军信息工程大学;2010年
2 苏继斌;基于渗透图的网络弱点评估研究[D];山东大学;2009年
3 井维亮;基于攻击图的网络安全评估技术研究[D];哈尔滨工程大学;2008年
4 吴昌;网络安全协议的高效分析系统[D];南昌大学;2008年
5 肖露娟;Web服务组合性能分析[D];浙江理工大学;2010年
6 邓珍荣;基于串空间模型的协议验证技术研究[D];广西大学;2005年
7 朱泽智;网络内容审计系统的研究与实现[D];北京邮电大学;2010年
8 殷珍珍;基于正则表达式的多模式匹配算法研究[D];杭州电子科技大学;2012年
9 王焕云;面向深度数据包检测的正则表达式匹配算法研究[D];湖南大学;2012年
10 谭志华;网络认证协议的高效模型检测研究[D];湖南大学;2011年
,本文编号:890001
本文链接:https://www.wllwen.com/guanlilunwen/ydhl/890001.html