Adaptation de la Génération Distribuée à la Volée des Espaces d’États aux Environnements Dynamiques / Zakaria Benmounah 

Public ISBD Titre : Adaptation de la Génération Distribuée à la Volée des Espaces d’États aux Environnements Dynamiques Type de document : texte imprimé Auteurs : Zakaria Benmounah, Auteur ; Anouar Boucheham, Auteur ; Djamel Eddine Saidouni, Directeur de thèse Editeur : CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine Année de publication : 2012 Importance : 133 f. Format : 30 cm. Note générale : Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Tolérance aux pannes, Plateforme Informatique Fondamentale  dynamique  Détection distribuée de la terminaison  Système distribué dynamique  Génération d’espaces d’états. Index. décimale : 004 Traitement de données. Informatique Résumé : L’utilisation des systèmes distribués peut être une bonne approche pour la résolution du problème de l’explosion combinatoire. Cependant, ces systèmes sont sujets à des changements dus à la dynamicité de la plateforme (panne, perte de messages, etc.). Au meilleur de nos connaissances, actuellement aucun travail n’a traité le problème de la distribution d’un espace d’états sous une plateforme dynamique. Nous proposons une approche permettant de résoudre le problème des pannes et l’intégration des machines durant le processus de génération distribuée des espaces d’états. Aussi, nous proposons un nouvel algorithme de détection de la terminaison qui tolère les pannes des machines Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7108 Adaptation de la Génération Distribuée à la Volée des Espaces d’États aux Environnements Dynamiques [texte imprimé] / Zakaria Benmounah, Auteur ; Anouar Boucheham, Auteur ; Djamel Eddine Saidouni, Directeur de thèse . - CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine, 2012 . - 133 f. ; 30 cm. Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Tolérance aux pannes, Plateforme Informatique Fondamentale  dynamique  Détection distribuée de la terminaison  Système distribué dynamique  Génération d’espaces d’états. Index. décimale : 004 Traitement de données. Informatique Résumé : L’utilisation des systèmes distribués peut être une bonne approche pour la résolution du problème de l’explosion combinatoire. Cependant, ces systèmes sont sujets à des changements dus à la dynamicité de la plateforme (panne, perte de messages, etc.). Au meilleur de nos connaissances, actuellement aucun travail n’a traité le problème de la distribution d’un espace d’états sous une plateforme dynamique. Nous proposons une approche permettant de résoudre le problème des pannes et l’intégration des machines durant le processus de génération distribuée des espaces d’états. Aussi, nous proposons un nouvel algorithme de détection de la terminaison qui tolère les pannes des machines Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7108

Réservation

Réserver ce document

Exemplaires (1)

Code-barres	Cote	Support	Localisation	Section	Disponibilité
MSINF120028	MSINF120028	Document électronique	Bibliothèque principale	Mémoires	Disponible

Documents numériques

texte integré Adobe Acrobat PDF

Approche Fonctionnelle pour la Mise en úuvre DistribuÈe de la SÈmantique OpÈrationnelle du Langage Temps-RÈel D-LOTOS / Amine Rihane 

Public ISBD Titre : Approche Fonctionnelle pour la Mise en úuvre DistribuÈe de la SÈmantique OpÈrationnelle du Langage Temps-RÈel D-LOTOS Type de document : texte imprimé Auteurs : Amine Rihane, Auteur ; Djamel Eddine Saidouni, Directeur de thèse Editeur : CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine Année de publication : 2011 Importance : 100 f. Format : 30 cm. Note générale : Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : SystËmes temps-rÈel, D-LOTOS, DATA*, compilation, programmation fonctionnelle, algorithmes distribuÈs Index. décimale : 004 Traitement de données. Informatique Résumé : Un systËme temps-rÈel comme tout systËme informatique doit fonctionner correctement, de ce fait, les techniques raisonnant sur la conformitÈ de ces systËmes sont indispensables. Parmi ces techniques, on peut citer les mÈthodes formelles ou techniques de description formelle. Ces mÈthodes permettent de rÈpondre aux exigences auxquelles sont soumis les systËmes temps-rÈel, et de raisonner rigoureusement ‡ líaide de logique mathÈmatique, sur des programmes informatiques, aÖn de prouver leur validitÈ par rapport ‡ une certaine spÈciÖcation. Les techniques de description formelle peuvent Ítre dÈÖnies comme un ensemble de notations dotÈes díune sÈmantique formelle et díoutils utilisÈs pour spÈciÖer sans ambiguÔtÈ le comportement des systËmes. Les sÈmantiques de vrai parallÈlisme, comme la sÈmantique de maximalitÈ, conviennent ‡ Ítre employÈes si on veut Èchapper ‡ líhypothËse de líatomicitÈ temporelle et structurelle des actions. Des travaux antÈrieurs ont montrÈ líimportance des modËles basÈs sur la maximalitÈ, ‡ titre díexemple, on peut citer le modËle sÈmantique DATA* pour la prise en compte explicite des durÈes díactions, des contraintes temporelles, de líurgence et líexpression du parallÈlisme. Dans une approche basÈe sur líÈvaluation de modËles (model checking), le systËme ‡ analyser doit Ítre spÈciÖÈ dans un modËle ou langage de spÈciÖcation de haut niveau. La spÈciÖcation rÈsultante est ensuite traduite vers un modËle sÈmantique. Notre travail qui síinscrit dans le cadre de la spÈciÖcation et la vÈriÖcation formelle des systËmes temps-rÈel, consiste en la mise en úuvre centralisÈe et distribuÈe de la sÈmantique opÈrationnelle du langage temps rÈel D-LOTOS, pour la gÈnÈration de structures appelÈes DATA* associÈs aux spÈciÖcations Ècrites dans le langage temps rÈel D-LOTOS. La rÈalisation de ce projet sera basÈe sur líutilisation du langage fonctionnel F# sous la plateforme Microsoft .Net. Par ailleurs líutilisation de cette plateforme a comme objectif la rÈalisation díun outil portable (indÈpendant du systËme díexploitation utilisÈ) ‡ travers le projet MONO qui rÈpond bien ‡ ce besoin. Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7525 Approche Fonctionnelle pour la Mise en úuvre DistribuÈe de la SÈmantique OpÈrationnelle du Langage Temps-RÈel D-LOTOS [texte imprimé] / Amine Rihane, Auteur ; Djamel Eddine Saidouni, Directeur de thèse . - CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine, 2011 . - 100 f. ; 30 cm. Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : SystËmes temps-rÈel, D-LOTOS, DATA*, compilation, programmation fonctionnelle, algorithmes distribuÈs Index. décimale : 004 Traitement de données. Informatique Résumé : Un systËme temps-rÈel comme tout systËme informatique doit fonctionner correctement, de ce fait, les techniques raisonnant sur la conformitÈ de ces systËmes sont indispensables. Parmi ces techniques, on peut citer les mÈthodes formelles ou techniques de description formelle. Ces mÈthodes permettent de rÈpondre aux exigences auxquelles sont soumis les systËmes temps-rÈel, et de raisonner rigoureusement ‡ líaide de logique mathÈmatique, sur des programmes informatiques, aÖn de prouver leur validitÈ par rapport ‡ une certaine spÈciÖcation. Les techniques de description formelle peuvent Ítre dÈÖnies comme un ensemble de notations dotÈes díune sÈmantique formelle et díoutils utilisÈs pour spÈciÖer sans ambiguÔtÈ le comportement des systËmes. Les sÈmantiques de vrai parallÈlisme, comme la sÈmantique de maximalitÈ, conviennent ‡ Ítre employÈes si on veut Èchapper ‡ líhypothËse de líatomicitÈ temporelle et structurelle des actions. Des travaux antÈrieurs ont montrÈ líimportance des modËles basÈs sur la maximalitÈ, ‡ titre díexemple, on peut citer le modËle sÈmantique DATA* pour la prise en compte explicite des durÈes díactions, des contraintes temporelles, de líurgence et líexpression du parallÈlisme. Dans une approche basÈe sur líÈvaluation de modËles (model checking), le systËme ‡ analyser doit Ítre spÈciÖÈ dans un modËle ou langage de spÈciÖcation de haut niveau. La spÈciÖcation rÈsultante est ensuite traduite vers un modËle sÈmantique. Notre travail qui síinscrit dans le cadre de la spÈciÖcation et la vÈriÖcation formelle des systËmes temps-rÈel, consiste en la mise en úuvre centralisÈe et distribuÈe de la sÈmantique opÈrationnelle du langage temps rÈel D-LOTOS, pour la gÈnÈration de structures appelÈes DATA* associÈs aux spÈciÖcations Ècrites dans le langage temps rÈel D-LOTOS. La rÈalisation de ce projet sera basÈe sur líutilisation du langage fonctionnel F# sous la plateforme Microsoft .Net. Par ailleurs líutilisation de cette plateforme a comme objectif la rÈalisation díun outil portable (indÈpendant du systËme díexploitation utilisÈ) ‡ travers le projet MONO qui rÈpond bien ‡ ce besoin. Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7525

Réservation

Réserver ce document

Exemplaires (1)

Code-barres	Cote	Support	Localisation	Section	Disponibilité
MSINF110027	MSINF110027	Document électronique	Bibliothèque principale	Mémoires	Disponible

Documents numériques

texte integré Adobe Acrobat PDF

Distribution adaptative d'un espace d'états Application aux STEMs et Réseaux de Petri / Ahmed Chaouki Chaouche 

Public ISBD Titre : Distribution adaptative d'un espace d'états Application aux STEMs et Réseaux de Petri Type de document : texte imprimé Auteurs : Ahmed Chaouki Chaouche, Auteur ; Djamel Eddine Saidouni, Directeur de thèse ; Jean Michel Ilie, Directeur de thèse Editeur : CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine Année de publication : 2011 Importance : 104 f. Format : 30 cm. Note générale : Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Distribution adaptative, voisinage, PSO, STEM, Réseaux de Petri, Génération à la volée. Index. décimale : 004 Traitement de données. Informatique Résumé : La vérication de systèmes informatiques est une nécessité de par leur ubiquité. Utilisés dans les domaines les plus critiques, lorsqu'ils sont défectueux, leur impact se mesure en vies humaines ou en pertes maté- rielles colossales. A cet eet, des techniques de vérication formelle performantes et de validation ecaces s'imposent dans la conception d'un système. La technique de vérication formelle la plus attractive du point de vue coût / performances est celle basée sur l'évaluation de modèles (model checking). Néanmoins, le facteur principal de limitation du model checking est le problème de l'explosion combinatoire de l'espace d'états. L'utilisation du modèle des systèmes de transitions étiquetées maximales (STEM) n'échappe pas à ce problème. An d'y remédier, la solution la plus ré- pandue, jusqu'à ce jour, est la distribution de l'espace d'états en vue de la répartition de la charge du calcul telles que la génération à la volée de l'espace d'états et la vérication de ses propriétés. An d'obtenir une meilleure distribution du graphe sur les diérents sites, nous proposons, dans le cadre de cette recherche, des algorithmes évolutionnaires issus de l'optimisation combinatoire s'inspirant essentiellement des phénomènes naturels tels que l'étude du comportement social des animaux évoluant en groupe (poissons, oiseaux ou abeilles) et cela en adaptant la méta-heuristique "Optimisation par Essaim Particulaire PSO" à la distribution des graphes. Permettant de trouver un compromis entre l'équilibrage de charge et la diminution des messages inter-sites. Par ailleurs, étant génériques, ces algorithmes, qui s'adaptent à n'importe quel graphe orienté, sont proposés pour traiter en particulier les systèmes de transitions, les systèmes de transitions étiquetées et les systèmes de transitions étiquetées maximales Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7736 Distribution adaptative d'un espace d'états Application aux STEMs et Réseaux de Petri [texte imprimé] / Ahmed Chaouki Chaouche, Auteur ; Djamel Eddine Saidouni, Directeur de thèse ; Jean Michel Ilie, Directeur de thèse . - CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine, 2011 . - 104 f. ; 30 cm. Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Distribution adaptative, voisinage, PSO, STEM, Réseaux de Petri, Génération à la volée. Index. décimale : 004 Traitement de données. Informatique Résumé : La vérication de systèmes informatiques est une nécessité de par leur ubiquité. Utilisés dans les domaines les plus critiques, lorsqu'ils sont défectueux, leur impact se mesure en vies humaines ou en pertes maté- rielles colossales. A cet eet, des techniques de vérication formelle performantes et de validation ecaces s'imposent dans la conception d'un système. La technique de vérication formelle la plus attractive du point de vue coût / performances est celle basée sur l'évaluation de modèles (model checking). Néanmoins, le facteur principal de limitation du model checking est le problème de l'explosion combinatoire de l'espace d'états. L'utilisation du modèle des systèmes de transitions étiquetées maximales (STEM) n'échappe pas à ce problème. An d'y remédier, la solution la plus ré- pandue, jusqu'à ce jour, est la distribution de l'espace d'états en vue de la répartition de la charge du calcul telles que la génération à la volée de l'espace d'états et la vérication de ses propriétés. An d'obtenir une meilleure distribution du graphe sur les diérents sites, nous proposons, dans le cadre de cette recherche, des algorithmes évolutionnaires issus de l'optimisation combinatoire s'inspirant essentiellement des phénomènes naturels tels que l'étude du comportement social des animaux évoluant en groupe (poissons, oiseaux ou abeilles) et cela en adaptant la méta-heuristique "Optimisation par Essaim Particulaire PSO" à la distribution des graphes. Permettant de trouver un compromis entre l'équilibrage de charge et la diminution des messages inter-sites. Par ailleurs, étant génériques, ces algorithmes, qui s'adaptent à n'importe quel graphe orienté, sont proposés pour traiter en particulier les systèmes de transitions, les systèmes de transitions étiquetées et les systèmes de transitions étiquetées maximales Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7736

Réservation

Réserver ce document

Exemplaires (1)

Code-barres	Cote	Support	Localisation	Section	Disponibilité
MSINF110046	MSINF110046	Document électronique	Bibliothèque principale	Mémoires	Disponible

Documents numériques

texte integré Adobe Acrobat PDF

Génération à la Volée des Graphes par Hybridation de la Fonction de Hachage MD5 et d’une Méta-heuristique / Chouaïb Chabil 

Public ISBD Titre : Génération à la Volée des Graphes par Hybridation de la Fonction de Hachage MD5 et d’une Méta-heuristique Type de document : texte imprimé Auteurs : Chouaïb Chabil, Auteur ; Mohamed Mehdi Benmoussa, Auteur ; Djamel Eddine Saidouni, Directeur de thèse Editeur : CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine Année de publication : 2012 Importance : 95 f. Format : 30 cm. Note générale : Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Explosion combinatoire de l’espace d’états, algorithmes distribués, graphes, distribution de graphes, fonction de hachage MD5, métaheuristique. Index. décimale : 004 Traitement de données. Informatique Résumé : La vérification formelle des systèmes informatiques est une des techniques les plus répandues utilisée dans le domaine des systèmes critiques. Un dysfonctionnement ou une erreur fonctionnelle négligeable rencontrée lors de la phase de l’exploitation de ceux-ci, est susceptible d’engendrer des pertes de vies humaines et/ou financières. A cet effet, pour éviter et surmonter l’occurrence de tels problèmes, des techniques de vérification formelle et de validation efficace s’imposent le long du processus de conception de ces systèmes. La méthode de vérification formelle la plus attractive et qui établit un bon compromis entre coût et performances est celle basée sur l’évaluation de modèle (en anglais Model Checking). Cependant, le model checking souffre du problème de l’explosion combinatoire de l’espace d’états, ce qui rend son utilisation contraignante du point de vu temps de calcul et espace de stockage. Dans le but de surmonter les limitations du model checker, la distribution de graphes ou de l’espace d’états est alors utilisée en vue de la répartition de la charge du calcul de génération de cet espace d’états et de son stockage sur les différents sites constituant le réseau. De même, des méthodes de vérification distribuées basées sur des espaces d’états distribués ont vu le jour et des recherches sont en cours pour améliorer leurs performances[JOUBERT, 2005, RIBET, 2005, Benamira, 2006, BOUNEB, 2011]. Les bonnes solutions de distribution de graphes sont celles qui équilibrent la charge de calcul entre les différents sites d’une part, et réduisent le maximum possible le nombre de connexions inter-sites. Dans ce contexte, nous proposons un nouvel algorithme basé sur l’hybridation de la fonction de hachage MD5 et d’une méta-heuristique que nous avons proposée. En outre, pour que l’algorithme soit générique, nous proposons une solution facilement adaptable à différents types de graphes orientés qui est destinée particulièrement pour traiter les systèmes de transitions, les systèmes de transitions étiquetées ainsi que les systèmes de transitions étiquetées maximales. Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7047 Génération à la Volée des Graphes par Hybridation de la Fonction de Hachage MD5 et d’une Méta-heuristique [texte imprimé] / Chouaïb Chabil, Auteur ; Mohamed Mehdi Benmoussa, Auteur ; Djamel Eddine Saidouni, Directeur de thèse . - CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine, 2012 . - 95 f. ; 30 cm. Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Explosion combinatoire de l’espace d’états, algorithmes distribués, graphes, distribution de graphes, fonction de hachage MD5, métaheuristique. Index. décimale : 004 Traitement de données. Informatique Résumé : La vérification formelle des systèmes informatiques est une des techniques les plus répandues utilisée dans le domaine des systèmes critiques. Un dysfonctionnement ou une erreur fonctionnelle négligeable rencontrée lors de la phase de l’exploitation de ceux-ci, est susceptible d’engendrer des pertes de vies humaines et/ou financières. A cet effet, pour éviter et surmonter l’occurrence de tels problèmes, des techniques de vérification formelle et de validation efficace s’imposent le long du processus de conception de ces systèmes. La méthode de vérification formelle la plus attractive et qui établit un bon compromis entre coût et performances est celle basée sur l’évaluation de modèle (en anglais Model Checking). Cependant, le model checking souffre du problème de l’explosion combinatoire de l’espace d’états, ce qui rend son utilisation contraignante du point de vu temps de calcul et espace de stockage. Dans le but de surmonter les limitations du model checker, la distribution de graphes ou de l’espace d’états est alors utilisée en vue de la répartition de la charge du calcul de génération de cet espace d’états et de son stockage sur les différents sites constituant le réseau. De même, des méthodes de vérification distribuées basées sur des espaces d’états distribués ont vu le jour et des recherches sont en cours pour améliorer leurs performances[JOUBERT, 2005, RIBET, 2005, Benamira, 2006, BOUNEB, 2011]. Les bonnes solutions de distribution de graphes sont celles qui équilibrent la charge de calcul entre les différents sites d’une part, et réduisent le maximum possible le nombre de connexions inter-sites. Dans ce contexte, nous proposons un nouvel algorithme basé sur l’hybridation de la fonction de hachage MD5 et d’une méta-heuristique que nous avons proposée. En outre, pour que l’algorithme soit générique, nous proposons une solution facilement adaptable à différents types de graphes orientés qui est destinée particulièrement pour traiter les systèmes de transitions, les systèmes de transitions étiquetées ainsi que les systèmes de transitions étiquetées maximales. Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7047

Réservation

Réserver ce document

Exemplaires (1)

Code-barres	Cote	Support	Localisation	Section	Disponibilité
MSINF120022	MSINF120022	Document électronique	Bibliothèque principale	Mémoires	Disponible

Documents numériques

texte integré Adobe Acrobat PDF

Mise en oeuvre centralisée de la sémantique opérationnelle des réseaux de petri temporellement temporisés réduite approche orientée objet / Ramla Benhamlaoui 

Public ISBD Titre : Mise en oeuvre centralisée de la sémantique opérationnelle des réseaux de petri temporellement temporisés réduite approche orientée objet Type de document : texte imprimé Auteurs : Ramla Benhamlaoui, Auteur ; Manel Maamar, Auteur ; Djamel Eddine Saidouni, Directeur de thèse Editeur : CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine Année de publication : 2011 Importance : 77 f. Format : 30 cm. Note générale : Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Syst`emes temps-r´eel, RdPTT, Mod`ele des DATA*’s, alpha-´equivalence Index. décimale : 004 Traitement de données. Informatique Résumé : Les m´ethodes formelles sont de plus en plus utilis´ees pour r´epondre aux exigences auxquelles sont soumis les syst`emes temps-r´eel. Ces m´ethodes reposent sur l’utilisation de mod`eles formels de sp´ecification dot´es de s´emantiques rigoureuses et de techniques de v´erification formelle. Il faut d’abord choisir un mod`ele de sp´ecification formelle, et de lui associer un mod`ele s´emantique qui servira `a sa v´erification formelle. Nous nous int´eressons `a la g´en´eration du graphe du comportement qui sera exploiter afin de v´erifier les propri´et´es qualitatives et/ou quantitatives requises du syst`eme. D’autre part, les s´emantiques de vrai parall´elisme, comme la s´emantique de maximalit´e, conviennent `a ˆetre employ´ees lorsqu’on s’abstrait de l’hypoth`ese de l’atomicit´e temporelle et structurelle des actions ; des travaux ant´erieurs ont largement montr´e l’aptitude du mod`ele DATA*(Durational Action Timed Automata) `a prendre en consid´eration et le comportement parall`ele des syst`emes et la prise en compte du temps. Parmi ces travaux, nous citons le mod`ele des r´eseaux de Petri temporellement temporis´es (RdPTT) dont le but est la sp´ecification des syst`emes temps-r´eel. Notre travail est une contribution `a la v´erification des syst`emes critiques concurrents. Il consiste `a r´ealiser l’outil qui impl´emente les r`egles de g´en´eration du mod`ele DATA* de mani`ere op´erationnelle `a partir du mod`ele RdPTT. Ainsi que son extension par l’impl´ementation de la alpha ´equivalence dans le processus de g´en´eration `a fin de surmonter le probl`eme de l’explosion combinatoire Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7567 Mise en oeuvre centralisée de la sémantique opérationnelle des réseaux de petri temporellement temporisés réduite approche orientée objet [texte imprimé] / Ramla Benhamlaoui, Auteur ; Manel Maamar, Auteur ; Djamel Eddine Saidouni, Directeur de thèse . - CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine, 2011 . - 77 f. ; 30 cm. Une copie electronique PDF disponible au BUC. Langues : Français (fre) Catégories : Informatique Tags : Syst`emes temps-r´eel, RdPTT, Mod`ele des DATA*’s, alpha-´equivalence Index. décimale : 004 Traitement de données. Informatique Résumé : Les m´ethodes formelles sont de plus en plus utilis´ees pour r´epondre aux exigences auxquelles sont soumis les syst`emes temps-r´eel. Ces m´ethodes reposent sur l’utilisation de mod`eles formels de sp´ecification dot´es de s´emantiques rigoureuses et de techniques de v´erification formelle. Il faut d’abord choisir un mod`ele de sp´ecification formelle, et de lui associer un mod`ele s´emantique qui servira `a sa v´erification formelle. Nous nous int´eressons `a la g´en´eration du graphe du comportement qui sera exploiter afin de v´erifier les propri´et´es qualitatives et/ou quantitatives requises du syst`eme. D’autre part, les s´emantiques de vrai parall´elisme, comme la s´emantique de maximalit´e, conviennent `a ˆetre employ´ees lorsqu’on s’abstrait de l’hypoth`ese de l’atomicit´e temporelle et structurelle des actions ; des travaux ant´erieurs ont largement montr´e l’aptitude du mod`ele DATA*(Durational Action Timed Automata) `a prendre en consid´eration et le comportement parall`ele des syst`emes et la prise en compte du temps. Parmi ces travaux, nous citons le mod`ele des r´eseaux de Petri temporellement temporis´es (RdPTT) dont le but est la sp´ecification des syst`emes temps-r´eel. Notre travail est une contribution `a la v´erification des syst`emes critiques concurrents. Il consiste `a r´ealiser l’outil qui impl´emente les r`egles de g´en´eration du mod`ele DATA* de mani`ere op´erationnelle `a partir du mod`ele RdPTT. Ainsi que son extension par l’impl´ementation de la alpha ´equivalence dans le processus de g´en´eration `a fin de surmonter le probl`eme de l’explosion combinatoire Diplome : Master 2 Permalink : https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7567

Réservation

Réserver ce document

Exemplaires (1)

Code-barres	Cote	Support	Localisation	Section	Disponibilité
MSINF110033	MSINF110033	Document électronique	Bibliothèque principale	Mémoires	Disponible

Documents numériques

texte integré Adobe Acrobat PDF

---

1 (1 - 5 / 5)