Gregorio Díaz Descalzo

La Mancha Real-Time and Concurrent Systems Group, University of Castilla, Spain.

Time: Thursday 9.3.2006, 14:30
Place: Room B2-109, Fr. Bajersvej 7

Model Checking of Web Services Choreographies and Orchestrations

In the last years some new techniques and languages for developing distributed application have appeared, such as the Extensible Markup Language, XML, and some new Web Services frameworks for describing interoperable data and platform neutral business interfaces, enabling more open business transactions to be developed.

Web Services cover a wide range of systems, which in many cases have strong time constraints (for instance, peer-to-peer collaborations may have time limits to be completed). Then, in many Web Services descriptions these time aspects can become very important. Actually, they are currently covered by the top level layers in Web Services architectures with elements such as time-outs and alignments. Time-outs allow each party to fix the available time for an action to occur, while alignments are synchronizations between two peer-to-peer parties.

Thus, it becomes important for Web Services frameworks to ensure the correctness of systems with time constraints. For instance, we can think in a failure of a bank to receive a large electronic funds transfer on time, which may result in huge financial losses. Then, there is growing consensus that the use of formal methods, development methods based on some formalism, could have significant benefits in developing E-business systems due to the enhanced rigor these methods bring. Furthermore, these formalisms allow us to reason with the constructed models, analyzing and verifying some properties of interest of the described systems. One of these formalisms are timed automata, which are very used in model checking, and there are some well-known tools supporting them, like UPPAAL.