采用动作时序逻辑的Web服务组合方法

摘要

Based on the theory of finite state automata (FSA), this paper models a Web service as an FSA. Firstly, it extends Web services description language (WSDL) for describing the behaviors of Web services, and proposes an algorithm for translating the extended WSDL to temporal logic of action (TLA) language; accordingly the behaviors of Web services can be described and normalized by using TLA, a new approach is provided to describe Web services in a formal way. Then, it discusses the composition way of FSA of each component service, and with the composition, how to compose such single service TLA specification to a composed service TLA specification, and on the basis of which, it proposes an algorithm to compose the TLA specifications correctly.%基于有限状态自动机理论,将Web服务建模成一个有限状态自动机.针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法.讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想.