Journée du 21 Mai 2010

Rubriques
Travaux en commun
Publications
Info. pratiques
Contacts
Séminaires
Le prochain

21/05/2010
05/03/2010
22/01/2010

04/12/2009
13/11/2009
02/10/2009
05/06/2009
03/04/2009
06/03/2009
23/01/2009

05/12/2008
14/11/2008
10/10/2008
30/05/2008
11/04/2008
21/03/2008
15/02/2008

Séminaires 2007

Séminaires 2006

Séminaires 2005


mod. 13-Jui-2010

Lieu

Telecom ParisTech, amphi Saphir: comment y aller

Programme

14h00-15h00: Rolf Hennicker, Ludwig-Maximilians-Universität München : "On Weak Modal Compatibility and Refinement of Modal I/O Transition Systems"

Abstract: Modal I/O automata (MIOs) by Larsen et al. provide a flexible framework for the specification and implementation of interacting systems. They distinguish between "may" transitions and "must" transitions, where the former can be disregarded and the latter must be respected by any correct refinement.

Building on the theory of MIOs we introduce a new compatibility notion, called weak modal compatibility, for interacting components. As an important property of behavioural interface theories we prove that weak modal compatibility is preserved under weak modal refinement. Then we extend the notion of weak modal compatibility to loosely coupled systems which interact via buffered FIFO channels. We show that also in this case weak compatibility is preserved by weak modal refinement and that, moreover, local refinements compose to global refinements. Finally, we describe the MIO Workbench, an Eclipse-based editor and verification tool for modal I/O automata.

15h00-15h30 : Christian Fotsing, LISI, ENSMA : "Modélisation de la prise en compte de la sémantique dans les applications temps-réel: concepts et outils"

transparentsAbstract: Nous considèrons les tâches comportant des instructions conditionnelles. Nous rappellons qu'il est important de tenir compte de façon explicite de ces instructions, afin d'avoir des résultats cohérents. Nous proposons donc une modélisation formelle des systèmes temps réel basée sur les réseaux de Petri pour la gestion de la sémantique des tests et des instructions. Le modèle de réseaux de Petri utilisé est un réseau autonome coloré fonctionnant sous la règle du tir maximal. Nous montrons enfin que le modèle proposé respecte bien les contraintes étudiées et modélise de façon plus réaliste les systèmes temps réel..

15h30-16h00: pause café

16h00-16h30: vie du groupe