论文部分内容阅读
随着面向服务的体系结构的发展，有效地组合单个分布的web服务以提供更有价值的服务成为新的热点问题。然而，在这一研究领域还存在诸多问题，比如web服务用哪种方式组合，能否实现自动组合，对组合服务进行正确性验证等等。文中主要是针对组合服务的正确性验证问题，引入时序逻辑TLA。通过把组合服务的BPEL描述转换为TLA可以理解的自动机的形式，这种方法可以很好地验证组合逻辑的正确性以及快速发现死锁等问题。