Semantics based analysis and synthesis of web services and workflows
Arthur J. Bernstein, Radu Grosu, Ziyang Duan · 2007
Web service technologies provide a standard platform based on which heterogeneous software applications can be integrated over the Internet. Web service protocols, such as WSDL, provide a standard way for software applications to communicate with each other. Web service orchestration languages, such as BPEL4WS, are proposed to specify business processes as workflows whose composite tasks are web services. In many cases, it is critical to verify the correctness of a business process before it is deployed, and it is also highly desirable that new business processes be automatically synthesized from available web services based on the business requirement. An abstract process model is introduced. The model restricts the data manipulation constructs in an abstract BPEL process. The restrictions permit a full description of a protocol while hiding computation details. A restricted abstract process can easily he converted into an abstract BPEL process or expanded into an executable process. A logic model is presented to formally specify the semantics of web services and workflows as abstract processes. A set of inference rules are established to deduce the strongest postcondition and weakest precondition of an abstract process. We demonstrate that the rules can be used for automatic inference due to the restriction on data manipulation capabilities in an abstract process. Based on this model, an algorithm is developed to automatically annotate the semantics and verify the correctness of workflows. An algorithm is developed to automatically synthesize a business process given its required semantics and a task library. The well-formedness of a task library is defined and the ranking assumption is introduced to simplify the synthesis procedure and guarantee its completeness. A prototype of the verification and synthesis system has been implemented and several business processes in the financial industry have been studied based on our approach. The model and algorithm is then extended to allow business rules to be specified and incorporated into the synthesis procedure.