WSCMon: runtime monitoring of web service orchestration based on refinement checking

摘要

Service-oriented systems, especially web services, have been given strong attention as an important approach to integrate heterogeneous systems, in which complex services are composed of simpler services offered by various service providers. The correctness of service composition requires techniques to verify whether composite services behave properly. To this end, in this paper, we propose a novel method for runtime monitoring of composite services. In our method, system specifications, which are automatically generated from descriptions of service composition, and requirement specifications, which include safety properties, are constructed to detect Business Process Execution Language (BPEL) engine-related and BPEL process-related violations. We employ process algebra as the primary formalism to express specifications. To verify the correctness of composite services, we check the refinement relation between specifications and observed behaviors. Also, we formally discuss what kinds of specifications can be monitored at runtime.