有界模型检测在服务组合中的应用研究

计算机工程与应用 ›› 2012, Vol. 48 ›› Issue (10): 111-114.

有界模型检测在服务组合中的应用研究

郝身刚，张丽

南阳师范学院计算机与信息技术系，河南南阳 473061

出版日期:2012-04-01 发布日期:2012-04-11

Research on service composition based on bounded model checking

HAO Shengang, ZHANG Li

Department of Computer and Information Technology, Nanyang Normal University, Nanyang, Henan 473061, China

Online:2012-04-01 Published:2012-04-11

摘要/Abstract

摘要： 大规模服务自动组合问题是Web Service技术的主要瓶颈。传统的服务组合技术灵活性差并且适用的服务规模有限。在用有限状态自动描述机服务的输入、输出、操作等活动的基础上，提出用有界模型检测技术对大规模服务进行建模，将用户请求翻译为线性时态逻辑公式，采用适定性问题求解技术快速求解限定长度的服务组合解。实验结果表明有界模型检测技术应用在自动服务组合中是可行的。

关键词: 有界模型检测, 服务组合, 线性时态逻辑, 适定性问题

Abstract: Large-scale automatic service composition is the main problem in Web Service technology.?The classic means of service composition have little flexibility and are applied in small-scale services.?Based on service description by using finite state machine, a way of bounded model checking techniques applied in modeling large-scale service composition is proposed, in which user requirements are translated into linear temporal logic formulas and the technology of solving satisfiability problem is used to discover the limited length composed solutions of services quickly.Experimental results show that it is feasiable to apply the techniques of bounded model checking to look for the solution of large-scale service composition.

Key words: bounded model checking, service composition, linear temporary logic, satisfiability

郝身刚，张丽. 有界模型检测在服务组合中的应用研究[J]. 计算机工程与应用, 2012, 48(10): 111-114.

HAO Shengang, ZHANG Li. Research on service composition based on bounded model checking[J]. Computer Engineering and Applications, 2012, 48(10): 111-114.

[1]	王亮1，2，郭星1，2. 基于柯西烟花算法的大规模服务组合优化[J]. 计算机工程与应用, 2018, 54(24): 34-40.
[2]	陈健，朱庆生，张程. QoS感知的语义服务组合搜索算法[J]. 计算机工程与应用, 2017, 53(2): 58-63.
[3]	汪潇洒1，付晓东1，刘骊1，岳昆2，刘利军1. 随机QoS感知的Web服务组合概率分析[J]. 计算机工程与应用, 2017, 53(14): 70-75.
[4]	贾志淳1，邢星1，2. 多Web服务组合兼容性的自动化验证[J]. 计算机工程与应用, 2016, 52(7): 67-73.
[5]	张驰，褚楚，唐颖军，陈升. 基于行为投影的Web服务组合行为兼容性研究[J]. 计算机工程与应用, 2016, 52(20): 46-51.
[6]	庄亚欧，徐汉川，徐晓飞，王忠杰，何霆. 基于服务模式的快速服务组合方法研究[J]. 计算机工程与应用, 2016, 52(1): 1-6.
[7]	许喆1，薛霄1，吕克林2. 物流服务的BPEL流程建模及组合算法研究[J]. 计算机工程与应用, 2015, 51(10): 53-59.
[8]	倪志伟1，2，尹道明1，2，王力1，2，李怀英1，2，王士凯1，2. 基于和声搜索算法的知识即服务动态组合优化[J]. 计算机工程与应用, 2012, 48(32): 212-217.
[9]	刘志中，薛霄，安吉宇，鲁保云. 基于LG-MMAS算法的制造云服务优化组合研究[J]. 计算机工程与应用, 2012, 48(25): 239-242.
[10]	董玲玲1，关永1，李晓娟1，施智平1，张杰2，华伟1. 用LTL模型检验的方法验证SpaceWire检错机制[J]. 计算机工程与应用, 2012, 48(22): 88-94.
[11]	梁志伟1，2，朱松豪1，金欣2. 分布式资源的Web服务组合机制[J]. 计算机工程与应用, 2012, 48(1): 68-71.
[12]	刘毅1，薛红超2，夏云霓2，杨骏1. 服务组合排编规范性能分析研究[J]. 计算机工程与应用, 2011, 47(22): 227-232.
[13]	朱晓红，贺亮，秦佳. 多服务副本下的一种分布式负载均衡路径算法[J]. 计算机工程与应用, 2011, 47(21): 105-108.
[14]	王飞明，董荣胜，胡元闯，骆翔宇. 全局优化的分层动态Web服务组合[J]. 计算机工程与应用, 2011, 47(12): 72-74.
[15]	李继民^1，2，刘振鹏²，刘志田²，韩磊². 多约束的Web服务组合研究[J]. 计算机工程与应用, 2010, 46(24): 110-114.