Towards Provably Correct Services: Automated Service Composition Via Supervisory Control Synthesis
Service-oriented computing (SOC) is a distributed computing paradigm that is revolutionizing the development of software systems. Service-oriented architecture (SOA) provides a framework for realizing and implementing SOC. A Web service is a key concept for developing SOA applications that allows interoperability among distributed software applications deployed on different platforms and architectures, which is important for many electronic business applications. Web services enable organizations to carry out certain business activities automatically and in a distributed fashion. However, in some circumstances, a single service is not able to perform a certain task and it becomes necessary to compose two or more services in order to complete it. Thus, a key research challenge in SOA is the problem of automated service composition. Several approaches exist that tackle the problem of automatic service composition; however, the task of generating provably correct Web service compositions still remains a challenging and complex task. The goal of this dissertation is to leverage the existing work on supervisory control to solve the problem of automated service composition with a focus on control and correctness. Therefore, in this dissertation, we develop a novel formal framework for modeling Web service compositions based on Supervisory Control Theory (SCT) of discrete-event systems. We model services that exchange messages and exhibit nondeterministic (runtime-dependent) behaviours based on runtime input. The objective is to synthesize a supervisor that interacts with a given set of Web services through messages to guarantee that a given specification is satisfied. The framework employs Labelled Transition Systems (LTSs) equipped with guards and data variables to model Web services and provides a technique to synthesize a controller. We model the interactions of services asynchronously and we use the guards and data variables to express certain preconditions which are then propagated from the system requirements through the overall composite service. The dissertation also provides a prototype implementation toolkit and an evaluation of the applicability of the approach using a number of case studies. A key novelty of this work is the application of control theory to service-oriented computing and the incorporation of runtime input into the supervisor generation process.
URI for this recordhttp://hdl.handle.net/1974/22789
Request an alternative formatIf you require this document in an alternate, accessible format, please contact the Queen's Adaptive Technology Centre
The following license files are associated with this item:
Except where otherwise noted, this item's license is described as Attribution-NonCommercial 3.0 United States
Showing items related by title, author, creator and subject.
Canadian Security Intelligence Service | Service Canadian du renseignement de Securite (Government of Canada, 2016-02)All reports and/or studies commissioned by CSIS on the agency's commitment to diversity (as defined by the Employment Equity Act) between January 1, 2010 and January 22, 2016.
Canadian Security Intelligence Service | Service Canadian du renseignement de Securite (Government of Canada, 2016-03)Reports dated May 1, 2013 to November 30, 2013 from ITAC, IAB or INSET concerning the shale gas protest in New Brunswick or mentioning Elsipogtog First Nation and/or Mi 'Kmaq Warriors Society.
ATIP Request: CSIS Director Briefing material for Senate National Security Committee appearance, April 20, 2015. Canadian Security Intelligence Service | Service Canadian du renseignement de Securite (Government of Canada, 2015-10)CSIS Director Briefing material for Senate National Security Committee appearance, April 20, 2015.