Please use this identifier to cite or link to this item:
Type: Theses
Title: Formal verification of transactional and configurable service-oriented processes
Author: Bourne, Scott Stanier
Issue Date: 2016
School/Discipline: School of Computer Science
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%.
Advisor: Sheng, Michael
Szabo, Claudia
Dissertation Note: Thesis (Ph.D.) -- University of Adelaide, School of Computer Science, 2016.
Keywords: web services
cloud computing
formal methods
transactional requirements
model checking
Provenance: This electronic version is made publicly available by the University of Adelaide in accordance with its open access policy for student theses. Copyright in this thesis remains with the author. This thesis may incorporate third party material which has been used by the author pursuant to Fair Dealing exceptions. If you are the owner of any included third party copyright material you wish to be removed from this electronic version, please complete the take down form located at:
Appears in Collections:Research Theses

Files in This Item:
File Description SizeFormat 
01front.pdf178.79 kBAdobe PDFView/Open
02whole.pdf2.72 MBAdobe PDFView/Open
  Restricted Access
Library staff access only201.42 kBAdobe PDFView/Open
  Restricted Access
Library staff access only2.67 MBAdobe PDFView/Open

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.