Correctness verification for service-based business processes

To keep up with the trend of globalization and informatization, an increasing number of enterprises decide to run their business process in a service-based manner with the help of Web Service technology. In order to manage such service-based business process (SBP), it is vital that the dependencies among the internal process and the exposed external services are correctly developed and maintained. SBP is dynamic by nature, therefore it is necessary to develop a practical and robust method to verify the correctness of SBP. In an SBP, complex dependencies exist not only between internal process and involved services but also within their components (activities, data, operations, etc.). The complex dependencies make the correctness verification for SBP a challenging task. In this work, we develop a correctness verification approach to handle this task. A Petri net based model is proposed with a hierarchical structure to cover the characteristics of SBPs. This model can support the control flow patterns that are necessary for SBPs. A set of correctness properties for SBP are identified which any SBP developers shall consider, and the respective verification methods are developed.