Introducing compositionality in webservice descriptions

Abstract. Web services are essentially black box components from a composer’s or a mediator’s perspective. The behavioural description of any service, can therefore be asserted by the composer, only through interface predicates exposed by the service provider through the service description. Normally for proving properties of service compositions, pre and post conditions are found to be sufficient and are specified for services described in languages like OWL-S. However these properties, are assertions only on the initial and final states of the service respectively. They do not help in specifying or verifying ongoing behaviour of an individual service or a composed system. In an environment, where services are black boxes, and composition is undertaken at runtime, it is necessary to have additional properties that can be asserted at various points during service execution to ensure that the composition would eventually result in one of the outcomes specified by the service provider. We propose a framework for enriching service descriptions with two additional assertions: assumption and commitment that facilitate compositional reasoning about services for the composition and verification of their integration. The technique is based on Interval Temporal Logic(ITL), a sound formalism for specifying and proving temporal properties of systems.