基于MAS模型检测与抽象的Web服务验证

发布时间：2017-11-06 05:02

  本文关键词：基于MAS模型检测与抽象的Web服务验证

  更多相关文章： Web服务组合 多主体系统 模型检测 图状反例 抽象 精化

【摘要】：Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统(MAS)模型检测工具(MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。
【作者单位】： 华侨大学计算机科学与技术学院;桂林电子科技大学广西可信软件重点实验室;
【基金】：国家自然科学基金资助面上项目(61170028) 华侨大学中青年教师科研提升计划基金资助项目(ZQN-YX109) 华侨大学高层次人才科研启动基金资助项目(11BS108) 广西可信软件重点实验室基金资助项目(kx201323)
【分类号】：TP393.09
【正文快照】： 中文引用格式:许兴旺,骆翔宇.基于MAS模型检测与抽象的Web服务验证[J].计算机工程,2015,41(3):26-31,36.1概述面向Web服务的软件开发已成为跨组织业务流程集成的关键技术。然而,单一Web服务功能有限,在多数情况下不能满足用户需求,因此出现将多个Web服务按某种特定组合集成为

【参考文献】

中国期刊全文数据库 前2条

1 骆翔宇;陈艳;;Web服务的形式化验证[J];计算机工程;2010年05期

2 骆翔宇;王昆;王凤钗;;一种Web服务组合的认知模型检测方法[J];小型微型计算机系统;2011年10期

【共引文献】

中国期刊全文数据库 前10条

1 俞东进;吴为;殷昱煜;闫大强;刘志清;;基于模型检测的服务规则路由正确性验证方法[J];电子科技大学学报;2014年01期

2 高洪皓;缪淮扣;曾红卫;;基于CEGAR的Web应用验证[J];计算机学报;2014年04期

3 Qian Junyan;Wu Juan;Zhao Lingzhong;Guo Yunchuan;;SUMMARIZATION OF BOOLEAN SATISFIABILITY VERIFICATION[J];Journal of Electronics(China);2014年03期

4 钱俊彦;赵岭忠;蔡国永;;基于完备抽象解释的性质强保留抽象研究[J];计算机学报;2014年08期

5 黄宏涛;王静;叶海智;黄少滨;;基于惰性切片的线性时态逻辑性质验证[J];吉林大学学报(工学版);2015年01期

6 化希耀;苏博妮;陈立平;高贤强;;模型检测技术研究综述[J];塔里木大学学报;2013年04期

7 范大娟;黄志球;肖芳雄;彭焕峰;李雯睿;;一种需求驱动的服务行为适配方法[J];四川大学学报(工程科学版);2014年02期

8 姚雪梅;艾颖;;基于SPIN求解狼和白菜过河问题[J];铜仁职业技术学院学报;2014年02期

9 赵会群;申宁;;Web服务组合编辑器的设计与实现[J];计算机技术与发展;2012年12期

10 彭蕾;;一种矛盾需求信息的建模方法[J];信息系统工程;2014年11期

中国博士学位论文全文数据库 前7条

1 田伟;模型驱动的web应用SQL注入安全漏洞渗透测试研究[D];南开大学;2012年

2 金洋;基于传递系统模型的在轨卫星故障诊断方法研究[D];哈尔滨工业大学;2013年

3 黄玉辉;配电网拓扑的形式化表达及其应用[D];上海交通大学;2013年

4 刘智;二进制代码级的漏洞攻击检测研究[D];电子科技大学;2013年

5 骆超;混沌和异步布尔网络中若干问题的研究[D];大连理工大学;2013年

6 袁敏;面向服务的业务事务建模与验证方法研究[D];南京航空航天大学;2012年

7 高明;知识协同工作流建模、服务规划和服务组合研究[D];东北财经大学;2013年

中国硕士学位论文全文数据库 前10条

1 谢雨;Web服务合作关系模型研究[D];中南大学;2012年

2 何霞;基于翻译模式的BPEL到LOTOS映射方法研究[D];北方工业大学;2013年

3 水晶;GSM-R在信号集中监测系统中的应用研究[D];兰州交通大学;2013年

4 王杰;USB3.0设备控制器IP核控制端点的RTL功能验证[D];合肥工业大学;2013年

5 张壹;C语言应用程序的静态漏洞检测[D];华中科技大学;2013年

6 万季;嵌入式软件缺陷检测的测试用例生成与排序研究[D];杭州电子科技大学;2014年

7 胡瀚月;面向C语言代码的规则检测工具研究[D];兰州理工大学;2014年

8 陈娟娟;基于双格的多值模型精化关系及对称化简[D];南京航空航天大学;2014年

9 许兴旺;基于多智能体系统模型检测与抽象技术的Web服务组合验证[D];华侨大学;2014年

10 屈丽;基于QoS证据数据库的服务合作关系研究[D];中南大学;2014年

【二级参考文献】

中国期刊全文数据库 前1条

1 骆翔宇;苏开乐;杨晋吉;;有界模型检测同步多智体系统的时态认知逻辑[J];软件学报;2006年12期

中国博士学位论文全文数据库 前1条

1 骆翔宇;多智能体系统的符号模型检测[D];中山大学;2006年

【相似文献】

中国期刊全文数据库 前10条

1 邝宏斌;罗贵明;;并行软件模型检测[J];计算机工程;2008年19期

2 周立青;杨晋吉;;乐观合同签订协议的模型检测分析[J];计算机工程;2011年07期

3 周从华;刘志锋;;具有过去时态算子的计算树逻辑模型检测[J];计算机工程;2007年22期

4 陈振宇;陶志红;KLEINE BüNING Hans;王立福;;变量极小不可满足在模型检测中的应用(英文)[J];软件学报;2008年01期

5 陈清亮;朱可宜;;多智能体协同的认知规范模型检测算法[J];中山大学学报(自然科学版);2009年01期

6 冯庆奎;;基于一阶迁移系统的限界模型检测工具实现[J];计算机工程与设计;2010年01期

7 骆翔宇;苏开乐;顾明;;一种求解认知难题的模型检测方法[J];计算机学报;2010年03期

8 韦林;古天龙;常亮;;基于模型检测的命题动态逻辑规划[J];桂林电子科技大学学报;2010年02期

9 刘剑,林惠民;传值进程模型检测中诊断信息的生成[J];软件学报;2003年01期

10 肖健宇;张德运;郑卫斌;张勇;;程序条件化用于软件模型检测中的状态空间缩减[J];西安交通大学学报;2006年04期

中国重要会议论文全文数据库 前7条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

6 邢立国;张光甫;刘薇;胥维昌;金一和;;人皮肤模型评价杀菌类农药腐蚀/刺激性研究[A];2014线粒体毒性与基于毒性通路的安全性评价新策略学术研讨会暨中国毒理学会毒理学替代法与转化毒理学专业委员会成立大会论文集[C];2014年

7 张明玉;;我国对外开放、通货膨胀与经济增长相关关系的模型检测[A];面向21世纪的科技进步与社会经济发展（下册）[C];1999年

中国博士学位论文全文数据库 前10条

1 江华;界程演算模型检测[D];贵州大学;2008年

2 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

3 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

4 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

5 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

6 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

7 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

8 黄宏涛;基于懒惰切片的模型检测技术研究[D];哈尔滨工程大学;2012年

9 刘金卓;基于符号化模型检测的软件演化过程模型验证[D];云南大学;2013年

10 吴骏;多Agent联盟规范系统研究[D];南京大学;2011年

中国硕士学位论文全文数据库 前10条

1 张衍志;符号化模型检测算法的研究[D];吉林大学;2009年

2 黎吾平;模型检测在软件方面的应用[D];吉林大学;2008年

3 吴小娟;并行完备模型检测技术的研究[D];电子科技大学;2013年

4 姜志敏;模型检测在配置中的应用[D];吉林大学;2010年

5 金怡爱;基于模型检测方法的规划[D];吉林大学;2005年

6 施小纯;基于反例搜索的启发式模型检测算法的研究[D];中国科学院研究生院（软件研究所）;2004年

7 陈亚军;模型检测在安全协议形式化验证中的应用[D];电子科技大学;2012年

8 高静;面向环境演算系统的模型检测算法的研究[D];南京航空航天大学;2009年

9 龚爱民;基于模型检测的模型驱动式开发系统的设计与实现[D];华东师范大学;2008年

10 黄丫;基于模型检测的可诊断性的形式化检验研究[D];吉林大学;2006年

，

本文编号：1147425