Dissertation for the degree of Doctor of Computer Sciencie to be presented with due permission of the Departament of Computer Science, for public examination and debate

Resumen

Abstract Nowadays, most computing systems are based on service-oriented computing (SOC). This paradigm aims at replacing complex monolithic systems by a composition of interacting systems called services. A service encapsulates a self-contained functionality o_ering it over a well-de_ned and standardised interface. It allows cross-organizational collabora- tions in which each participant is in charge of a particular task leading to the development of scalable, exible and low-cost distributed applications. Each service works as an au- tonomous component, performing only the tasks for which it has been implemented. As the development of such services is independent, companies can reuse a considerable amount of components, thus saving money and time. Moreover, these technologies are widely used due to their ability to provide interoperability among services from di_erent companies, since all the participants know the services o_ered by the others, as well as how to access them. Due to privacy concerns or commercial policy, entities participating in one of these architectures have no access to complete information, that is, the code implementing the consumed services is hidden, thus being impossible to examine or verify the implementation of the consumed services. Another issue is that web services are usually stateless, which means that no state is stored from the clients viewpoint. However, some new applications and services have emerged, which require to capture the state of some resources. Thus, new standards to manage the state of a web service have appeared. For instance, Open Grid Services Infrastructure (OGSI) was conceived to allow designers to manage resources when using web services, and this standard became Web Services Resource Framework (WSRF), where new improvements were introduced. Obviously, in this scenario the probability of making errors is higher than working in a monolithic scenario. Therefore, there is a clear need of applying any speci_c techniques to ensure the correctness of each participant and their composition. In this Thesis, we _rst present a formal language called BPELRF and its semantics. The aim of this language v is to model a set of business processes implemented in the de-facto standard modelling language, WS-BPEL, but enriched with the ability to manage distributed resources. These distributed resources are managed according to the guidelines provided by the standard WSRF. Moreover, we provide a visual model of this language in terms of coloured Petri nets in order to ease uninitiated people to deal with it, and we use the well-known toolbox, CPNTools, to verify the composition of web services with distributed resources expressed in BPELRF. As usual, the process of building manually the Petri nets model of large scenarios is time-consuming and error-prone. Therefore, we have implemented a tool to support web designers that, given a BPELRF speci_cation, it extracts automatically the coloured Petri nets of the scenario. Finally, this model can be veri_ed using CPNTools. On the second part of the Thesis, we extend the classical de_nition of Workow nets with time features. Workow nets were introduced by Wil van der Aalst as a formalism for the modelling, analysis and veri_cation of business workow processes. The formalism is based on Petri nets, but abstracting away most of the data while focusing on the possible ows in the system. Then, the main purpose of using workow nets is to _nd early design errors such as the presence of deadlocks, livelocks and other anomalies in workow processes. Such correctness criteria can be described via the notion of soundness, which requires the option to complete the workow, guarantees proper termination and optionally also the absence of redundant tasks. After the seminal work on workow nets, researchers have invested much e_ort in de_n- ing new soundness criteria and/or improving the expressive power of the original model by adding new features and studying the related decidability and complexity questions. In this Thesis, we de_ne a quantitative extension of workow nets with timing features, called timed-arc Workow nets. These allow us to argue, among others, about the ex- ecution intervals of tasks, deadlines and urgent behaviour of workow processes. Our workow model is based on timed-arc Petri nets, where tokens carry timing information and arcs are labelled with time intervals restricting the available ages of tokens used for transition _ring. Here, we consider both discrete and continuous time semantics, thus conforming a whole theory of workow nets. This timed Petri net extension is currently supported by the tool TAPAAL, thus o_ering to researchers and users a potential mean to model timed-arc workow nets and to automatically verify (strong) soundness.