Les travaux de l’équipe s’intéressent à la modélisation et à la vérification des systèmes temps réels complexes par l’utilisation de méthodes formelles rigoureuses. Notons que les systèmes temps réels sont souvent au coeur d’applications critiques telles que l’avionique, les systèmes intégrés sur puces, les centrales nucléaires,…etc. D’ailleurs, il est envisagé l’application de ces techniques pour la validation de systèmes spécifiques, types embarqués, tolérants aux fautes et multimédia. Pour ce besoin, différentes approches sont explorées par les membres de l’équipe :
MR HAMMAL propose dans le cadre de la formalisation du langage orienté objet UML, des méthodes et des modèles pour définir de manière rigoureuse la sémantique des différents diagrammes UML avec prise en considération des aspects temporels.
Cette formalisation vise la vérification de la consistance (sémantique et temporelle) des modèles UML.
Ses travaux s’intéressent aussi à l’analyse des systèmes concurrents à base de composants et en particulier aux problèmes de compatibilité et de substituabilité des composants.
Finalement, un dernier intérêt est porté à l’étude des méthodes générales et formelles de comparaison entre les langages et modèles du parallélisme.
Les travaux de MR ABDELLI tendent à définir un modèle unificateur à base de réseau de Pétri permettant de modéliser les systèmes temps réels à contraintes faibles ou fortes, proposant des synchronisations de différents nivaux, et des mécanismes de préemption temporelle voire de ressources. Cela implique de :
Définir rigoureusement la syntaxe et la sémantique du modèle.
D’analyser ces systèmes par énumération de leur espace d’état, en proposant aussi bien des algorithmes calculant des abstractions exactes préservant leurs propriétés linéaires voire de branchements, que des heuristiques de moindre coût calculant des approximations préservant un sous ensemble de propriétés inhérentes à leur sûreté.
A d’autres égards, d’exploiter ces approches pour la conception et la proposition de techniques adaptées pour la gestion et l’amélioration de la qualité de service des applications multimédia. Des techniques de pré-chargement et de gestion du buffer sont explorées pour être implémentées à différents niveaux (Client, proxy, ou Serveur).
Les travaux de Melle MAZOUZ s’inscrivent dans le cadre de la vérification modulaire des systèmes Informatiques et particulièrement les systèmes temps réels, afin de palier au problème d’explosion combinatoire de l’espace d’état. Cela implique :
De définir un modèle permettant une spécification modulaire à base de réseaux de Petri temporels ; ce dernier est basé sur une sémantique à temps discret.
De définir un algorithme calculant le graphe modulaire ; ce dernier est constitué des graphes d’états partiels des modules et un graphe de synchronisation qui capture les communications entre modules.
Ses travaux abordent aussi le problème de l’analyse modulaire proprement dit. Dans ce contexte, il a été développé une approche de vérification modulaire de certaines propriétés génériques telles que l’accessibilité, le blocage et la vivacité d’un réseau de Petri temporel modulaire.
Actuellement, une approche modulaire des réseaux de Petri temporels dans le cadre d’une sémantique dense est explorée.
Les travaux de MR BENKAOUHA s’intéressent, à définir et à valider des protocoles de détection de défaillances dans les systèmes répartis particulièrement dans les réseaux mobiles. En effet, la tolérance aux fautes est primordiale pour assurer la continuité du service et particulièrement dans le cas de la mobilité. Cet environnement est connu pour être très vulnérable aux pannes. Par conséquent, la proposition de solutions efficaces passe par la mise en oeuvre de techniques exploitant des mémoires stables et des protocoles de calcul de points de contrôle ainsi que le recouvrement.