========================================================================

Séminaire MeFoSyLoMa http://www.mefosyloma.fr/

Méthodes Formelles pour les Systèmes Logiciels et Matériels

vendredi 28 Mars 2014, 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/access-lrde.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 Laura Carnevali - Université de Florence, "Quantitative evaluation of non-Markovian models through the approach of stochastic state classes: applications and future issues"

Abstract: The method of stochastic state classes supports steady state and transient analysis of models that encompass multiple timers with general distribution and possibly bounded support. When the model underlies a Markov Regenerative Process (MRP) that always reaches a regeneration point within a finite number of steps, transient analysis can be limited to the first regeneration epoch and repeated from every regenerative point. This supports efficient derivation of the local and global kernels that characterize the MRP behavior and enables transient evaluation through the numerical integration of generalized Markov renewal equations. Applications of the approach through the Oris Tool are illustrated referring to the evaluation of availability measures for maintenance procedures. Future research directions are discussed in the area of probabilistic schedulability analysis of real-time systems.

15h00-15h30 Ridha Benosman - CNAM, "Conception et Évaluation de Performances d'un Bus Applicatif Parallèle et Orienté Service"

Abstract: De nombreuses solutions d'intégration d'applications à base d'ESB on été proposées. Cependant, ces solutions d'intégration ne supportent pas le traitement parallèle. et ne tirent donc pas profit des technologies multicoeurs. Nous proposons une solution de type "bus" permettant le traitement parallèle. Pour cela, nous avons conçu et mis en oeuvre : un mécanisme de multiplexage/démultiplexage en mesure de contrôler la circulation du flux de données, un allocateur dynamique de mémoires partagées répondant à certaines limitations du standard des mémoires IPC et un nouveau connecteur permettant à l'ensemble des threads d'une même application mère de fonctionner simultanément sur des zones mémoires complètement disjointes.

15h30-16h00: Pause café

16h00-16h30: Vie du groupe

========================================================================