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

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

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