Laboratoire MISC

Modélisation et Implémentation des Systèmes Complexes

Equipe CFSC

Présentation

L’équipe s’intéresse à la conception et à la vérification des systèmes critiques, tel que les protocoles de communication, les systèmes embarqués et les systèmes temps réel de manière particulière. Des travaux antérieurs ont déjà permis à l’équipe de développer plusieurs modèles de spécification formelle des systèmes critiques ainsi que des modèles sémantiques utilisés comme domaines d’interprétation des modèles de spécification (bissimulations, logiques temporelles ou test formel). L’équipe a ainsi défini le langage temps réel D-LOTOS muni d’une sémantique de vrai parallélisme à savoir la sémantique de maximalité, ainsi que la proposition de deux modèles sémantiques permettant la prise en compte des durées d’actions et les contraintes temporelles, ces deux modèles sont le modèle des DATAs (Durational Action Timed Automata) et le modèle des DATA*s utilisé pour exprimer la sémantique du langage D-LOTOS. Sur ces modèles, les chercheurs de l’équipe continueront à développer des méthodes de vérification basées sur différentes approches, comportementales, logiques et tests.

Membres

Chef d'équipe

  • Djamel Eddine Saïdouni

Membres permanents

  • Farid Arfi
  • Mokdad Arous
  • Nabil Belala
  • Adel Benamira
  • Messaouda Bouneb
  • Zine El-Abidine Bouneb
  • Mourad Bouzenada
  • Mohamed Khergag
  • Ilhem Kitouni
  • Sofia Kouah
  • Riad Lakhchine
  • Toufik Marouk

Thésards LMD

  • Imen Benstira
  • Kenza Bouaroudj
  • Imededdine Chama
  • Ahmed Chawki Chaouche
  • Souad Guellati
  • Hiba Hachichi
  • Riad Matmat
  • Nedjoua Saidane
  • Nacer Tabib

Activités scientifiques (2009-2012)

Thèses de Doctorat en Sciences soutenues:

  1. Toufik Messaoud Marouk, Modèles formels pour la conception des systèmes temps réel. Université Mentouri Constantine, Juin 2012.  Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  2. Zine Elabidine Bouneb, Vérification symbolique des systèmes critiques :Approche distribuée. Université Mentouri Constantine, Mars 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  3. Nabil Belala, Modèles de temps et leur intérêt à la vérification formelle des systèmes temps réel. Université Mentouri Constantine, Octobre 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  4. Abdesslem Layeb, Utilisation des approches d’optimisation combinatoire pour la vérification des applications temps réel. Mentouri Constantine, Mai 2010.  Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.

Thèses de Magister soutenues:

  1. Abd Elouahab Khiar. « Génération du code java à partir de spécifications D-LOTOS étendu », 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  2. Amel Boumaza, Algorithmes de model checker opérant sur les DATA* (Durational Action Timed Automata). Université Mentouri Constantine, Novembre 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  3. Mohamed KHERGAG, Interprétation de spécifications D-LOTOS étendu en terme d’automates temporisés avec durées d’actions, Centre universitaire de Khenchla, Année 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  4. Khaled DJABER, Vérification formelle des systèmes temps réel. Centre universitaire El Oued, Année 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  5. Nadjoua SAIDANE,Un système d’aide au diagnostic médical dans un environnement temps réel et critique. Université Mentouri Constantine, Année 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI
  6. Messaouda Bouneb,Vérification comportementale des réseaux de Petri sous une sémantique de maximalité. Université Oum El-Bouaghi, Algérie., Février 2009. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI
  7. Hamza Ghougha, Méthode évolutionnaire quantique pour la vérification des systèmes concurrents. Université de Tébessa, Algérie. Janvier 2009. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI
  8. Ilhem Kitouni, Déterminisation des automates temporisés avec durées d'actions pour le test formel. Université Mentouri Constantine, Algérie, Décembre 2008. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI

Mémoires de Master soutenus:

  1. Chouaib Chabil et Mohamed Mehdi Benmoussa. « Génération à-la-volée des graphes par hybridation de la fonction de hachage MD5 et d’une méta-heuristique ». Université Mentouri de Constantine, Juin 2012. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  2. Zakaria Benmounah et Anouar Boucheham. « Adaptation de la génération distribuée à-la-volée des espaces d’états aux environnements dynamiques ». Université Mentouri de Constantine, Juin 2012. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  3. Ahmed Chaouki Chaouche. « Distribution adaptative d’un espace d’états, Application aux STEMs et Réseaux de Pétri  ». Juin 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  4. Asma Chachoua et Radja Boukharrou. « Mise en œuvre distribuée de la sémantique opérationnelle des réseaux de Pétri temporellement temporisés : Approche Orientée Objet ».Juin 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  5. Fatima Bourbia et Sara Boukerzaza. « Application de l’approche de transformation de graphes pour la génération de l’automate de région minimal à partir de DATA* ». Juin 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  6. Ramla Benhamlaoui et Manel Mâamar.« Mise en œuvre centralisée de la sémantique opérationnelle des réseaux de Pétri temporellement temporisés  alpha-réduite : Approche Orientée Objet ». Juin 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  7. Amine Rihane. « Approche Fonctionnelle pour la Mise en œuvre distribuée de la sémantique opérationnelle du langage temps-réel D-LOTOS ». Juin 2011. Directeur de thèse : Pr Djamel Eddine SAIDOUNI.
  8. Mohamed Zaki Chellali et Bachir Djoudi. « Passage DATA* vers AutomatesTemporisés : Mise en Œuvre et Application ». Juin 2011. Directeur de thèse : Dr Nabil BELALA.
  9. Wassila Slougui et Yasmina Abid Charef.« Conception Formelle du Protocole SSH ». Juin 2011. Directeur de thèse : Dr Nabil BELALA.
  10. Khaoula Guessasma et Khadidja Benouareth. « Approches pour le Calcul Distribué : Application au Data Mining ». Juin 2011. Directeur de thèse : Dr Nabil BELALA.
  11. Asma Mezari et Dounia Benamira.« Système de Détection de Feu : Conception Formelle et Simulation ». Juin 2011. Directeur de thèse : Dr Nabil BELALA.
  12. Karima Sedrati et Abla Segueni, Vérification des systèmes temps réel exprimés en DATA* (Durational Action Timed Automata) par UPPAAL et KRONOS. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  13. Asma Benmehdi et Seifeddine Belbel, Transformation d’un micro-ordinateur Linux en un routeur avancé. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  14. Mohamed Saleh Ouaheb et Abderrahim Kaidi, Utilisation des approches d’optimisation combinatoire pour la vérification des applications concurrentes. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  15. Seif Elislam Bourouissa et Charaf Eddine Benameur,Génération distribuée de stems pour les réseaux de Petri.Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Djamel Eddine SAIDOUNI.
  16. Amira Mordjana et Fatima Zohra Saih, Protocole RTSP : Conception formelle et simulation. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Nabil BELALA.
  17. Amina Belala et Samira Messaoudi, Protocole PPP : Conception formelle et simulation. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Nabil BELALA.
  18. Asma Lakroune et Wafa Kifouche, Protocole SIP : Conception formelle et simulation. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Nabil BELALA.
  19. Aboubakeur Mérabti, Protocole DCCP : Conception formelle et simulation. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Nabil BELALA.
  20. Imene Zédairi et Billel Mezhoud,  DNS : Conception formelle et simulation. Université Mentouri Constantine, Juin 2010. Directeur de thèse : Dr. Nabil BELALA.

Mémoires d'Ingénieur soutenus:

  1. Ahlem BOUNEB : Définition d’une sémantique de maximalité pour les réseaux de Petri récursifs. Université Mentouri Constantine, Juin 2010. Encadreur Dr. Djamel Eddine SAIDOUNI.
  2. Amina Dib et Samiya Barkou,  Génération des stems distribué alpha réduit. Université Larbi Benmhidi, Juin 2010.Directeur de projet :Bouneb Zine Elabidine.
  3. Nedjoua Feddaoui, Zina Kabouche et Samah Allag,  Génération de stems à partir de la sémantique dénotationnelle d’une spécification LOTOS. Université Larbi Benmhidi, Juin 2010.Directeur de projet : Bouneb Zine Elabidine.
  4. Nora Belkadi et Mounia Hadjou,  Gestion de la paie. Université Larbi Benmhidi, Juin 2010.Directeur de projet : Bouneb Zine Elabidine.
  5. NacereddineMokdad, Environment of distance teaching integrated for intelligent sicio-constructivist platform. Centre Universitaire Abbas Laghrour, Khenchela, Juin 2010. Directeur de projet: Maarouk Toufik.
  6. Bezza Asma et Messas Amina, Développement d’un environnement de spécification des systèmes temps-réel en D-LOTOS. Centre Universitaire Abbas Laghrour, Khenchela, Juin 2010. Directeur de projet: Maarouk Toufik.

Comité de programme

  • SEFM 2008
  • SEFM 2009
  • Notere 2008
  • Notere 2009
  • ICADIWT 2008, Ostrava, August 4-6, 2008, Czech Republic
  • ICADIWT 2009, London, UK.
  • SNIB 2010
  • ICIST 2011
  • MISC 2010
  • MISC 2012