Séminaires

Le prochain

07/06/2024
22/03/2024
12/01/2024

10/11/2023
15/09/2023

11/06/2021

20/12/2019
11/10/2019
24/05/2019
22/03/2019
25/01/2019

Séminaires 2018
Séminaires 2017
Séminaires 2016
Séminaires 2015
Séminaires 2014
Séminaires 2013
Séminaires 2012
Séminaires 2011
Séminaires 2010
Séminaires 2009
Séminaires 2008
Séminaires 2007
Séminaires 2006
Séminaires 2005


mod. 09-09-2024

Séminaire du 03 Juin 2005

Lieu

LIPN

Programme

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.