The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Sessions are a central paradigm in Web services, as they allow the implementation of decentralized transactions with multiple participants. Sessions enable the cooperation of workflows while at the same time avoiding the mixing of workflows from distinct transactions.
Several languages such as BPEL, ORC, AXML have been proposed to implement Web Services. Sessions are usually implemented by attaching unique identifiers to transactions. The expressive power of these languages makes the properties of the implemented services undecidable.
In this talk, we propose a new formalism for modelling web services. Our model is session-based, but avoids using session identifiers. The model can be translated to a dialect of Petri nets that allows the verification of important properties of web services in terms of coverability in Petri nets.
This is joint work with Philippe Darondeau and Loic Helouet.