Deciding Service Substitution - Termination guaranteed
Published on 10. December 2012
Book
Paperback/Softback
180 pages
978-3-8439-0738-5 (ISBN)
Description
Service-oriented computing (SOC) supports the loose coupling of heterogenous software components. Each component is implemented as a service that encapsulates its specific functionality behind a well-defined interface. A key issue in the field of SOC is the ability to substitute one service by a refined version without harming the functionality of the overall system. Services are stateful and communicate asynchronously. On that account, the decision whether the overall system after substituting a service is still correct is by far not trivial.
In this thesis, we investigate behavioral service substitution. Thereby, we focus on the termination of the composed system and differentiate between weak termination and strong termination. Weak termination demands that it is always possible to reach a final state from every state of the system. Strong termination additionally requires that a final state is indeed reached. Our results show that in order to decide strong termination of a system, each involved service needs to define a fairness specification. In contrast, weak termination does not demand any kind of additional specification beside the definition of the service behavior. We use finite state automata that are tailored toward the modeling of services to formalize the behavior of a service.
The aim of service orientation is to compose a service P with other services R such that their composition terminates. We refer to each such service R as a controller of P. Within this thesis, we consider a special kind of service substitution: whether service P´ accords with service P under weak or strong termination. Accordance demands that every controller of P is a controller of P´ and, thus, no environment of P can distinguish between these two services. Deciding accordance is challenging because these sets of controllers may be infinite. To overcome the issue of comparing infinite sets, we propose the operating guideline as a finite representation of all controllers of a service with respect to one of the termination criteria. This data structure provides the basis of a finite algorithm to decide accordance for both weak and strong termination. Here, we define the refinement of operating guidelines and consider only services P and P´ without taking any particular controller into account. Therewith, we solve an open issue and provide a solution to one of the most prominent SOC research challenges.
In this thesis, we investigate behavioral service substitution. Thereby, we focus on the termination of the composed system and differentiate between weak termination and strong termination. Weak termination demands that it is always possible to reach a final state from every state of the system. Strong termination additionally requires that a final state is indeed reached. Our results show that in order to decide strong termination of a system, each involved service needs to define a fairness specification. In contrast, weak termination does not demand any kind of additional specification beside the definition of the service behavior. We use finite state automata that are tailored toward the modeling of services to formalize the behavior of a service.
The aim of service orientation is to compose a service P with other services R such that their composition terminates. We refer to each such service R as a controller of P. Within this thesis, we consider a special kind of service substitution: whether service P´ accords with service P under weak or strong termination. Accordance demands that every controller of P is a controller of P´ and, thus, no environment of P can distinguish between these two services. Deciding accordance is challenging because these sets of controllers may be infinite. To overcome the issue of comparing infinite sets, we propose the operating guideline as a finite representation of all controllers of a service with respect to one of the termination criteria. This data structure provides the basis of a finite algorithm to decide accordance for both weak and strong termination. Here, we define the refinement of operating guidelines and consider only services P and P´ without taking any particular controller into account. Therewith, we solve an open issue and provide a solution to one of the most prominent SOC research challenges.