Formal verification of transactional and configurable service-oriented processes

Abstract

The industrial rise of Web services and cloud services provides ample opportunities for business processes to be implemented with third-party components in a way that is rapid to develop, low-cost, and with reduced start-up risk. Service-oriented processes are business processes implemented by remotely provisioning third-party services: autonomous black box implementations of common software or hardware requirements. However, executing a workflow structure of these distributed and heterogeneous components creates several transactional concerns. These include ensuring an acceptable level of atomicity over long-running executions, handling a diverse range of potential fault types, and considering the various transactional properties of component services. In this thesis, we present three related approaches towards ensuring well-formed transactional behavior in service-oriented processes. We address the problem of identifying issues in the transactional behavior of service-oriented processes at design-time, to prevent costly issues or redevelopment at later stages. We adapt an expressive service-oriented process modeling approach that allows for developers to specify detailed transactional behavior. A set of rules can be applied to this model in order to identify transactional issues such as deadlock and invalid termination. Furthermore, developers can elicit complex and varied transactional requirements for the process with ease using our set of temporal logic templates. Model checking is used to ensure that process designs satisfy these rules and requirements. Recent innovations in cloud services have led to the proposal of Business Process as a Service (BPaaS). BPaaS offers common business processes as configurable cloud services, enabling clients to perform complex or resource expensive business operations in a simple pay-be-use manner. Both service providers and clients have concerns to be satisfied during BPaaS configuration. Providers must enforce domain constraints to restrict the service to valid configurations, while the client has their own application-dependent requirements for the service to meet. Using Binary Decision Diagram (BDD) analysis and model checking as formal methods, we devise a multi-step process that identifies a BPaaS configuration satisfying the requirements of both parties. These verification and configuration techniques have been implemented in a prototype tool called TL-VIEWS. We include six validation scenarios to demonstrate the effectiveness of our methods, using real Web and cloud services. An extensive performance analysis is performed for each model checking feature used by TL-VIEWS and the results indicate that our state-space reduction measures can decrease verification time for complex models by up to 98.63%.