Séminaires
Séminaire du 21 Mai 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"
Abstract: 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..