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.