A specification logic for dynamic composition of services

We focus on a composition model for services, which are composed of pre-programmed service components represented as Java classes. A common formal basis for representing the semantics of dynamic composition of services from service components is presented. We propose a logic and a specification language that enable us to reason about and deploy service components automatically. The proposed composition model uses a logical proof as witness for the correct deployment of service components in the context of their use. The composition model has been implemented in Java as an environment for dynamic composition of services. We illustrate the proposed composition method on an example of composition of a service