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 - 1 / 1)