Contractual verification of web service compositions with time constraints

Resumen

This chapter has described the state of the art of Service-Oriented Computing (SOC), the formalization of Web Service compositions, and the specification of electronic contracts (e-contracts). The development of systems based on Web Services allows the creation of fast, low-cost, flexible and scalable applications, where the integration is possible thanks to the definition of multiple standard protocols (WSDL, SOAP, UDDI). However, the correct composition of Web Services is still an open problem, where different approaches can be followed, such as orchestration (BPEL) and choreography (WS-CDL, WSCI, OWL-S). The formal analysis of Web Service compositions by means of formal methods is therefore necessary to guarantee the correct composition. Several formal techniques can be used for the analysis of Web Service compositions, being model checking one of the most popular. This is an automated technique consisting of the construction of a finite-state model of the system to check if some properties are satisfied. Different specification formalisms can be used in model checking (process algebras, Petri nets, automata) and there are several tools supporting each one of these formalisms (CWB-NC, CPN Tools, UPPAAL). E-contracts are used in the field of Web Service compositions as an agreement specifying how the services can interact, improving in this way the confidence when it is consumed a service provided by another entity. Different approaches 48 Chapter 2. State of the Art can be followed for the specification of e-contracts (Service-Level Agreements, behavioural interfaces, deontic e-contracts), but common goals must be fulfilled by all the approaches, such as the identification of dependencies and inconsistencies between clauses, the management of conflicts, etc. The formalization of e-contracts is an important research to carry out, in order to check the correctness of the e-contracts and the conformance of systems with respect to contract definitions. Multiple approaches can be found in the literature for this purpose, but additional efforts are still needed to cope with all the different problems that are related to this field.