Time: Thursday 9.3.2006, 14:30
Place: Room B2-109, Fr. Bajersvej 7
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.