======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/j2012-05-04.html Méthodes Formelles pour Les Systèmes Logiciels et Matériels Vendredi 4 mai 2012, 14h-17h Adresse : Epita, Amphi 4 (derrière la verrière à gauche dans la cour) 24 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : http://maps.google.fr/maps?q=48.815379,2.363139 http://www.lrde.epita.fr/~adl/dl/lrde-amphi4.pdf ======================================================================== 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 (Amphi 4) : Serge Haddad (LSV) Synthesis and Analysis of Product-form Petri Nets For a large Markovian model, a “product form” is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1) we provide a sound and complete set of rules for the synthesis; (2) we characterise the exact complexity of classical problems like reachability; (3) we introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed. 15h00-15h30 (Amphi 4) : Samira Chaou (LACL) Modélisation et analyse d'un système de notation dans un système de stockage pair-à-pair. Dans un système de stockage de données distribué, la disponibilité des données est une propriété critique à assurer. Pour analyser la robustesse du système de stockage UbiStorage on a procédé à l'évaluation de ce dernier en présence d'attaquants internes en utilisant la simulation. Pour résoudre le problème de perte de données ainsi détecté, un système de réputation est mis en place. Dans cet exposé, nous allons voir l'utilisation du formalisme ABCD pour la modélisation du système de stockage pair-à-pair d'UbiStorage et la modélisation des différentes attaques ainsi que du système de notation. Nous allons aussi voir les résultats d'analyse par model-checking du système de notation. 15h30-16h00 (LRDE) : pause café Elle aura lieu dans la bibliothèque du LRDE, au 18 rue Pasteur (2e étage). 16h00: vie du groupe (dans une salle voisine). ======================================================================== -- Alexandre Duret-Lutz