12 May
2015
12 May
'15
2:34 p.m.
========================================================================
Séminaire MeFoSyLoMa
http://www.mefosyloma.fr/
Méthodes Formelles pour les Systèmes Logiciels et Matériels
vendredi 22 mai 2015, 14h-17h
Adresse:
LRDE (EPITA), Salle Alpha
Bâtiment X, 2e étage
18 rue Pasteur, 94270 Le Kremlin-Bicêtre
Métro Porte d'Italie
Plans d'accès :
https://www.google.com/maps?q=48.8152808,2.3623765
https://www.lrde.epita.fr/~adl/dl/acces-lrde.pdf
S'il y en a parmi vous qui comptent venir en voiture, le parking du
centre commercial Okabé est gratuit pendant 3h.
http://www.okabe.com/okabe/fr/okabe-parking
========================================================================
Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires
Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC),
LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de
Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la
confrontation de différentes approches ou points de vue sur
l'utilisation des méthodes formelles dans les domaines du génie
logiciel, de la conception de circuit, des systèmes répartis, des
systèmes temps-réel ou encore des systèmes d'information. Il
s'organise autour de réunions bimestrielles où sont exposés des
travaux de recherche récents sur ce thème.
========================================================================
Programme
14h00-15h00: Ekkart Kindler, Denmark Technical University,
"Coordinating Interactions: The Event Coordination Notation"
Abstract: The purpose of a domain model is to concisely capture the
concepts of an application's domain, and their relation among each
other. Even though the main purpose of domain models is not
implementing the application, major parts of an application can be
generated from the application's domain models fully automatically
with today's technologies. The focus of most of today's code
generation technologies, however, is on the structural aspects of
the domain; the domain's behaviour is often not modelled at all,
implemented manually based on some informal models, or the behaviour
is modelled on a much much more technical level.
The Event Coordination Notation (ECNO) allows modelling the
behaviour of an application on a high level of abstraction that is
closer to the application's domain than to the software realizing
it. Still, these models contain all necessary details for actually
executing the models and for generating code from them.
In this talk, the limitations of today's modelling notations for
behaviour are briefly discussed. Then, the main idea, philosophy,
and concepts of ECNO and its notation are discussed -- mostly by
looking at some examples. The ECNO is now fully supported by a tool
which allows to generate code from ECNO models.
15h00-16h00: Ryszard Janicki, McMaster University,
"Modeling Concurrency With Interval Traces"
Abstract: Interval order structures are triples (X,≺,⊏) where X is a
set of event occurences and ≺, ⊏ are abstractions of 'earlier than'
and 'not later than' relationships.
Interval order structures are useful tools to model abstract
concurrent histories, i.e. sets of equivalent system runs, when
system runs are modeled with interval orders and we want to express
not only standard causality but also 'not later than'.
It turns out that interval order structures can be modeled by
partially commutative monoids, called interval traces, that are some
special case of general Mazurkiewicz traces. This new model will
then be used to provide a full semantics of Petri nets with
inhibitor arcs.
16h00-16h30: pause café
16h30-17h00: vie du groupe
========================================================================