Séminaire du 03 Juin 2005




14h00-15h00: Jonathan Billington (University of South Australia) Modelling and Analysis of TCP's Connection Management Procedure

Abstract: the Transmission Control Protocol (TCP) is the most widely used transport protocol in the Internet, providing a reliable data transfer service to many applications. This talk will present results of analysing TCP's Connection Management procedures for correct termination and absence of deadlocks. The protocol is assumed to be operating over a reordering lossless channel and is modelled using Coloured Petri nets. The following connection management scenarios are examined using state space analysis: client-server and simultaneous opening; orderly release; and abortion. I shall discuss a deadlock we discovered when connection release is initiated before the connection has been fully established.

15h00-15h30 : Sylvain Rampacek (LAMSADE et université de Reims) A formal semantics for Web services interaction

Abstract: Web Service protocols have been developed originally for standard communication or interface description of service (e.g. SOAP, WSDL). Currently, the effort go to behavioural description of Web Services, so as to be able to use them in a transactional context. We will study the XLANG and BPEL4WS language to show how its formalisation with a timed process algebra enables us to analyse it and to control its execution by a client (being a final user or another service). More precisely, our approach first defines a formal semantics for such languages. After an initial discrete time semantics, we have now developed a dense time semantics expressed with timed automata. We have devised generic algorithms to generate timed automata of Web services from their descriptions. In a second step, we define an adapted interaction relation (nearly equivalent to bisimulation) between client and services. Finally, we construct a client timed automaton corresponding to this interaction relation, starting from the service automata. During the construction, we also check if such a client automaton may be defined.

15h30-16h00: pause café

16h00-17h00: Fabrice Kordon (LIP6), Laure Petrucci (LIPN), Nicolas Trèves (CNAM) Petri nets normalisation: the ISO/IEC 15909 status

Abstract: we will present the status of ISO/IEC 15909 normalisation process, with a particular focus on the advancement of part 2. It will summarise the discussions taking place at the editorial meeting in Helsinki the week before the seminar. The current work and future trends will also be explained.