基于扩展投影时序逻辑的组合Web服务描述与验证 (2007年)

针对编制方式生成的组合Web服务需要用一个工作流引擎执行这个特征，对投影时序逻辑进行了扩展，并用扩展投影时序逻辑描述和验证组合Web服务。将组合Web服务视为一个基于过程的工作流，将工作流引擎与组合Web服务组成部分的一次不可分割的消息交互抽象为一个原子过程。用扩展投影时序逻辑公式描述原子过程，用扩展投影时序逻辑操作符定义过程组合规则、连接过程描述公式，得到组合Web服务描述公式。通过模拟组合Web执行，可验证组合Web服务满足系统的需求和性质，为提高组合Web服务设计的可靠性提供了依据。