======================================================================== 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 ========================================================================