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

Specification and Verification of Composite Web Services Based on Extended Projection Temporal Logic

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

According to the feature that the execution of web services composed by orchestration is completed by a workflow execution engine, the projection temporal logic is extended. An ap- proach based on this extended projection temporal logic （EPTL） for the specification and verifica- tion of composite web services is proposed. A composite web service is regarded as a processbased workflow. An indivisible message exchange between the workflow execution engine and a component of the composite web service is extracted as an atomic process represented by an EPTL formula. The connection rules of the processes are defined by the EPTL operators which connect the formulae representing processes to obtain new formulae representing composite web services. With simulating the execution of composite web services, whether services satisfy system requirements and properties can be verified. Therefore, this approach provides the basis for improving the reliability of the design of composite web services.