Souheib BAARIR   J'ai réalisé ma thèse (en informatique), sous la direction du Pr. Serge HADDAD, dans l'équipe Modélisation et Vérification (MoVe) du Laboratoire d'Informatique de Paris 6 (LIP6). Thèse soutenue le 16/05/2007 (Mémoire). J'ai, aussi, exercé la fonction d'attaché temporaire pour l'enseignement et la recherche à l'université de Paris X (de 2005 à 2007). J'ai réalisé un post-doc au département d'informatique de l'université du Piemonte orientale en Italie (Università degli Studi del Piemonte Orientale "Amedeo Avogadro", Alessandria, Italie), sous le thème de la "modélisation et l'évaluation de performance des systèmes distribués", et sous la direction de Mme. le Prof. Giuliana Franceschinis (Oct. 2007 à Jui. 2008). J'ai réalisé un post-doc dans l'équipe Architecture et Logiciels pour Systèmes Embarqués (ALSOC) du Laboratoire d'Informatique de Paris 6 (LIP6). Actuellement, Maitre de Conférences à l'Université de Paris Nanterre. J'effectue mes recherches au Laboratoire d'Informatique de Paris 6 (LIP6), dans l'équipe Modélisation et Vérification (MoVe).

Mes Recherches

Le thème de mes recherches s'inscrit dans le cadre des méthodes formelles de vérification de systèmes concurrents. L'évolution de ces systèmes se caractérise par une complexité croissante et un rôle toujours plus critique. Les logiciels orchestrant de tels systèmes doivent réagir correctement et en particulier face aux situations critiques.

La mise au point des applications réparties critiques est un problème complexe pour lequel il est recommandé d'utiliser des techniques de description formelle afin de spécifier sans ambiguïté le comportement des applications considérées. Il faut aussi des outils de vérification automatique ou semi-automatique afin de valider le bon fonctionnement de ces applications.

Les méthodes formelles de spécification de systèmes ont pour objectif d'assurer la fiabilité de ces logiciels, c'est-à-dire leur bonne spécification et l'absence d'erreur. Idéalement, pour concevoir le logiciel d'un système concurrent donné, il faudrait spécifier formellement ce système à l'aide d'un modèle mathématique à partir duquel on pourrait raisonner et vérifier les propriétés attendues.

Le principal obstacle pour mener à bien cette vérification est l'explosion combinatoire du nombre d'états possibles des systèmes. Malgré les avancées spectaculaires de la technologie des ordinateurs, il arrive que l'on soit incapable d'analyser intégralement des systèmes par manque d'espace ou de temps. Le défi est donc de proposer des modèles qui soient suffisamment expressifs pour décrire la réalité des systèmes, tout en restant raisonnablement analysables.

Mes Publications

Contact

Cette page a été mise à jour le 05/06/2012.