Recherches     Enseignements     Publications    Contact    

Souheib BAARIR

  

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

Revues internationales

 

  • Souheib Baarir, Cécile Braunstein, Emmanuelle Encrenaz, Jean-Michel Ilié, Isabelle Mounier, Denis Poitrenaud and Sana Younes. Feasibility analysis for robustness quantification by symbolic model checking. Formal Methods in System Design Journal, 2011, DOI : 10.1007/s10703-011-0121-5.

 

  • Souheib Baarir, Marco Beccuti, claude Dutheille, Giuliana Franceschinis and Serge Haddad. Lumping partially symmetrical stochastic models. Performance Evalutation Journal, Volume 68, Number 1, Pages 21-44, Januray 2011.

 

  • S. Baarir, M. Beccuti, D. Cerotti, M. De Pierro, S. Donatelli and G. Franceschinis. The GreatSPN Tool: Recent Enhancements. ACM Performance Evaluation Review, Volume 36, Number 4, March 2009.

Revues nationales

 

  • Julien Sopena, Souheib Baarir, Fabrice Legond-Aubry. Véfrication formelle d'un algorithme gérnérique et hiérachique d'exclusion mutuelle . Numéro spécial "Réseaux de Petri et algorithmes" du journal Technique et Science Informatique (TSI), vol. 28, pages 1085-1105, 2009, Lavoisier, France.

 

  • Yann Thierry-Mieg, Souheib Baarir, Alexandre Duret-Lutz, Fabrice Kordon. Nouvelles techniques de model-checking pour la vérification de systèmes complexes. Revue Génie Logiciel,n° 69, pp 17-23, 2004.

Chapitres de livres

 

  • Yann Thierry-Mieg, Jean-Michel Ilié, Souheib Baarir. Méthodes formelles pour les systèmes répartis et coopératifs-Vérifications efficace des systèmes finis. Chapitre 8, pp 171-207. Hermès Science Publications, 2006. ISBN : 2746214474.

Conférences et workshops internationaux

 

  • S. Baarir, C. Braunstein, E. Encrenaz, J.M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes. Quantifying Robustness by Symbolic Model checking. In proceedings of the 1st HardWare Verification Workshop (HWVW'10, CAV workshop). Juil. 2010.

 

  • Souheib Baarir, Marco Beccuti, Claude Dutheillet and Giuliana Franceschinis. From partially to fully lumped Markov chains in Stochastic Well Formed Petri Nets In Proceedings of the 4th International Conference on Performance Evaluation Methodologies and Tools (Valuetools'09). Oct. 2009.

 

  • S.Baarir, C.Braunstein, R.Clavel, E.Encrenaz, J.M.Ilié, R.Leveugle, I.Mounier, L.Pierre, D.Poitrenaud. Complementary Formal Approaches for Dependability Analysis, IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems (DFT'09), Oct. 2009.

 

  • Souheib Baarir, Marco Beccuti, Giuliana Franceschinis. New solvers for asymmetric systems in GreatSPN. In Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems (QEST'08), pages 235-236, Sep. 2008.

 

  • Souheib Baarir, Julien Sopena, Fabrice Legond-Aubry. Verification of a Hierarchical Generic Mutual Exclusion Algorithm. In Proceedings of the 28th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'08), pages 99-115, June 2008.

 

  • Souheib Baarir, Alexandre Duret-Lutz. Emptiness check of powerset Büchi automata. In Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD'07), pages 41-50, July 2007.

 

  • Marco Beccuti, Souheib Baarir, Giuliana Franceschinis, Jean-Michel Ilié. Efficient lumpability check in partially symmetric systems. International Conference on the Quantitative Evaluation of Systems (QEST'06), pp 211-220, Sep. 2006.

 

  • Souheib Baarir, Claude Dutheillet, Serge Haddad, Jean-Michel Ilié. On the use of exact lumpability in partially symmetrical Well-formed Nets. International Conference on the Quantitative Evaluation of Systems (QEST'05), pp 23-32, Sep. 2005 (Best paper award).

  • Souheib Baarir, Jean-Michel Ilié et Alexandre Duret-Lutz. Improving Reachability Analysis for Partially Symmetric High Level Petri Nets. Poster Session of the International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pp 5-8, Sep. 2004.

 

  • Souheib Baarir, Serge Haddad et Jean-Michel Ilié. Exploiting Partial Symmetries in Well-formed nets for the Reachability and the linear Time Model Checking Problems. International Workshop on Discrete Event Systems (WODES'04), pp 223-228, Sep. 2004.

 

  • J-M Ilié, S. Baarir, M. Beccuti, C. Delamare, S. Donatelli, C. Dutheillet,  G. Franceschinis, R. Gaeta,  P. Moreaux. Extended SWN Solvers in GreatSPN. International Conference on the Quantitative Evaluation of Systems (QEST'04), pp 324-325, Sep. 2004.

 

  • Jérome Hugues, Yann Thierry-Mieg, Fabrice Kordon, Laurent Pautet, Souheib Baarir, Thomas Vergnaud. On the Formal verification of Middleware Behavioral Proprties. International Workshop on Formal Methods for Industrial Critical Systems (FMICS'04), pp 139-157, Sep. 2004.

 
  • Okba Kazar, Souheib Baarir. Générateur de Plan pour un robot. In Proceedings of International Conference on Productic (CIP'01), pp. 55-65, Algiers, 09-11, June 2001.

Conférences nationales

 
  • Souheib Baarir, Alexandre Duret-Lutz. Test de vacuité pour automates de Büchi ensemblistes avec tests d'inclusion. In Actes du 6e Colloque Francophone sur la Modélisation des Systèmes Réactifs (MSR'07), pages 19-34, October 2007.

Rapports techniques

 
  • Souheib Baarir, Alexandre Duret-Lutz. Emptiness Check of Powerset Büchi Automata using Inclusion Tests. Technical report 2006/003, Université Pierre et Marie Curie, LIP6-CNRS, Paris, France, 2006.

Mes Enseignements (PARIS X)

Contact

Université Pierre et Marie Curie
Bureau 26/25-208
4 place Jussieu,
75252 Paris Cedex 05.
Tél : 01 44 27 71 05
E-mail : souheib.baarir@lip6.fr		 UFR SEGMI, Université Paris Ouest Nanterre La Défense
Bâtiment G - Bureau E37,
200 avenue de la République,
92001 Nanterre Cedex.
Tél : 01 40 97 73 95
E-mail: souheib.baarir@u-paris10.fr

Cette page a été mise à jour le 30/10/2010.