For a system of distributed processes, correctness can be ensured by (statically) checking whether their composition satisfies properties of interest. However, Web services are distributed processes that dynamically discover properties of other Web services. Since the overall system may not be available statically and since each business process is supposed to be relatively simple, we propose to use runtime monitoring of conversations between partners as a means of checking behavioral correctness of the entire Web service system. Specifically, we identify a subset of UML 2.0 Sequence Diagrams as a property specification language and show that it is sufficiently expressive for capturing safety and liveness properties. By transforming these diagrams to automata, we enable conformance checking of finite execution traces against the specification. We show how our language can be used to specify the Specification Property System (SPS) [1]. We describe an implementation of our approach as part of an industrial system. Finally, we discuss our experience of specifying and monitoring a number of properties from three existing applications.

Service level agreements (SLAs) impose many non-functional requirements on services. Business analysts specify and check these requirements in business process models using tools such as IBM WebSphere Business Modeler. System integrators on the other hand use service composition tools such as IBM WebSphere Integration Developer to create service composition models, which specify the integration of services. However, system integrators rarely verify SLA compliance in their proposed composition designs. Instead, SLA compliance is verified after the composed services are deployed in the field. To improve the quality of the composed services, we propose a framework to verify SLA compliance in composed services at design time. The framework re-uses information in business process models to simulate services and verify the non-functional requirements before the service deployment. To demonstrate our framework, we built a prototype using an industrial process simulation engine from IBM WebSphere Business Modeler and integrate it into an industrial service composition tool. Through a case study, we demonstrate that our framework and the prototype assist system integrators in composing services while considering the non-functional requirements.