计算机科学与探索 ›› 2011, Vol. 5 ›› Issue (3): 208-220.
周 宁1,2, 刘 慧3, 王红兵3, 谢俊元1,2
ZHOU Ning1,2, LIU Hui3, WANG Hongbing3, XIE Junyuan1,2
摘要: 基于有限状态自动机理论, 将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展, 提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法, 从而可以用TLA对服务行为进行形式化描述和规范, 为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中, 服务组合时各组件服务的有限状态自动机的组合方式, 以及伴随着服务组合, 单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题, 并在此基础上, 提出了实现TLA规范正确组合的算法思想。