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.