Mohamed MOSBAH
Mohamed Mosbah Professeur (ENSEIRB)

Équipe LaBRI : Méthodes formelles
Fonction administrative : Directeur Adjoint Resp. Relations Industrielles
Page personnelle : http://www.labri.fr/~mosbah
Courrier électronique : mohamed.mosbaharobaselabri.fr
Bureau : 363
Tél : +33 (0)5 40 00 69 17


Recherche

Mes activités de recherche concernent l'utilisation des transformations de graphes comme modèle de calcul pour construire et
étudier des familles d'algorithmes. Après mes travaux sur des familles d'algorithmes sur des classes de graphes décomposables, je
m'intéresse actuellement à la mise au point d'un modèle de description, d'étude et d'analyse d'algorithmes distribués.

D'un point de vue théorique, je m'intéresse à certains problèmes comme : l'élection, le nommage, le calcul d'un arbre recouvrant, la
détection de la terminaison, la synchronisation, le consensus ou bien la reconnaissance de certaines propriétés du réseau.  Ces
études sont faites d'une part en fonction des règles de calcul autorisées sur le réseau et d'autre part de la connaissance initiale ou de
la configuration initiale du réseau. Le codage d'algorithmes comme réécriture de graphes nous a permis d'obtenir des résultats
nouveaux dans le domaine de l'algorithmique distribuée. En particulier, j'ai obtenu un nouvel algorithme distribué, efficace en termes
de complexité, de partitionnement d'un graphe en clusters. J'ai également étudié plusieurs paradigmes de l'algorithmique distribuée
dans ce même modèle: agents mobiles, tolérances aux pannes, synchronisation. Récemment, je m'intéresse à l'utilisation des
techniques
de preuves formelles pour la correction d'algorithmes distribués codés
par des réécritures de graphes. Dans le cadre d'une collaboration avec le LORIA (Nancy), nous avons développé des techniques de
preuves qui utilisent le raffinement et mis au point plusieurs preuves complètes d'algorithmes distribués. Par ailleurs, en formalisant
le modèle de réécriture de graphes en Coq, nous avons obtenu des résultats concernant des classes d'algorithmes: Nous avons
montré qu'il n'existe pas d'algorithme d'élection de la classe LC0 (réécriture de deux sommets adjacents) dans un arbre non décoré
(sans connaissance initiale du degré).

D'un point de vue expérimental, on accompagne nos travaux par la réalisation d'un environnement logiciel permettant
d'implémenter, de visualiser les graphes et leurs transformations et les calculs distribués qui s'exécutent sur ces graphes. Cet
environnement est utilisé en recherche (pour tester des nouveaux algorithmes) mais aussi en enseignement (étudiant de masters). Le
logiciel visidia fait également l'objet d'un travail de collaboration avec l'université de Pretoria en Afrique du Sud.

Extrait de publications


Pierre Castéran, Vincent Filou, Mohamed Mosbah. Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant. Symbolic Computation in Software Science (SCSS 2009), Sep 2009, Tunisia. To appear, 2009.

Amine Haddar, Ahmed Hadj Kacem, Yves Métivier, Mohamed Mosbah, Mohamed Jmaiel. A Distributed Computational Model for Mobile Agents. 10th Pacific Rim International Workshop on Multi-Agents, Nov 2007, Bangkok, Thailand. Springer, 5044, pp.417-421, 2009, Lecture Notes in Artificial Intelligence.

Imen Jemili, Abdelfattah Belghith, Mohamed Mosbah. Exploiting a clustering mechanism for power saving in ad hoc networks: Performance evaluation. IEEE/ACS International Conference on Computer Systems and Applications, 2009. AICCSA 2009., May 2009, Rabat, Morocco. IEEE Computer Science, pp.717-724, 2009,

Bilel Derbel, Mohamed Mosbah, Akka Zemmari. Sublinear Fully Distributed Partition with Applications. Theory of Computing Systems, Springer Verlag, 2010, 47 (3), pp.368-404.


Responsabilité pédagogique

- Responsable de l'option Génie Logiciel, 3ème A., ENSEIRB-MATMECA (IPB)

Administration

Depuis 2010: Directeur adjoint du LaBRI,
Depuis 2009: Directeur des Relations Industrielles de l'ENSEIRB-MATMECA (IPB)

Valorisation

2006-2009: RIMEL, ANR Sécurité Informatique, Coordinateur local,
2008-2010: RECORDS, Projet labellisé, FUI, Coordinateur local,
2010-2013: SIMID, Projet labellisé, FUI, Coordinateur local


Page mise à jour le 13/08/2010 à 10:56