|
|
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.
Université Pierre et Marie Curie Bureau 26/25-208 4 place Jussieu, 75252 Paris Cedex 05. Tél : 01 44 27 61 92 E-mail : souheib.baarir@lip6.fr |
UFR SEGMI, Université Paris Nanterre 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@parisnanterre.fr |
Cette page a été mise à jour le 05/06/2012.