Towards Provably Correct Services: Automated Service Composition Via Supervisory Control Synthesis

Abstract

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.