University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur Mourad kezai |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la recherche
Titre : Transcription des spécifications M-UML vers le système Maude Type de document : texte imprimé Auteurs : Mourad kezai, Auteur ; Khababa,Abdellah, Directeur de thèse Année de publication : 2023 Importance : 1 vol (157 f .) Format : 29cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : système Maude
LTL (Linear Time Logic)Index. décimale : 004 Informatique Résumé :
Les systèmes multi-agents forment un type intéressant de modélisation de sociétés, car ils ont des domaines d'application très larges. Par conséquent, le domaine de la technologie des "agents mobiles" représente un concept nouveau et important en intelligence artificielle et de l'ingénieries de logiciels. Malgré l'intérêt porté à cette technologie, la plupart des approches à l'heure ne permettent pas une conception suffisante et complète des agents mobiles.
D'autre part, Maude est un environnement de spécification, de programmation orientée objet et de preuve basé sur une logique de réécriture qui est un cadre sémantique unificateur de plusieurs modèles de concurrence. En plus, le système Maude dispose également d'une batterie d'outils permettent la simulation, l’analyse d'accessibilité par le LTL (Linear Time Logic) Model-checker permettant la vérification et le prototypage des propriétés de spécification.
Enfin, la méthode graphique UML généralement et ses extensions permettent de représenter de manière synthétique et intuitive les systèmes multi-gent. Cependant, elles ne sont pas dotées permettant de faire la vérification. Dans cette thèse, nous adoptons une approche de la spécification formelle des diagrammes M-UML dans le système Maude. Nous avons appliqué notre approche en trois étapes proposées au diagramme d'états-transitions, l'un des diagrammes les plus importants de M-UML. La technique consiste à dériver systématiquement une description formelle de Maude à partir de ce type d'analyse de diagramme, et nous avons obtenu des résultats très satisfaisants. Cette transcription proposée permet d'obtenir une spécification algébrique exprimée en logique de réécriture. Ce dernier sera utilisé pour vérifier les spécifications des systèmes à base d'agents mobiles.Côte titre : DI/0075 En ligne : http://dspace.univ-setif.dz:8888/jspui/bitstream/123456789/4095/1/Mourad%20Kezai [...] Format de la ressource électronique : Transcription des spécifications M-UML vers le système Maude [texte imprimé] / Mourad kezai, Auteur ; Khababa,Abdellah, Directeur de thèse . - 2023 . - 1 vol (157 f .) ; 29cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : système Maude
LTL (Linear Time Logic)Index. décimale : 004 Informatique Résumé :
Les systèmes multi-agents forment un type intéressant de modélisation de sociétés, car ils ont des domaines d'application très larges. Par conséquent, le domaine de la technologie des "agents mobiles" représente un concept nouveau et important en intelligence artificielle et de l'ingénieries de logiciels. Malgré l'intérêt porté à cette technologie, la plupart des approches à l'heure ne permettent pas une conception suffisante et complète des agents mobiles.
D'autre part, Maude est un environnement de spécification, de programmation orientée objet et de preuve basé sur une logique de réécriture qui est un cadre sémantique unificateur de plusieurs modèles de concurrence. En plus, le système Maude dispose également d'une batterie d'outils permettent la simulation, l’analyse d'accessibilité par le LTL (Linear Time Logic) Model-checker permettant la vérification et le prototypage des propriétés de spécification.
Enfin, la méthode graphique UML généralement et ses extensions permettent de représenter de manière synthétique et intuitive les systèmes multi-gent. Cependant, elles ne sont pas dotées permettant de faire la vérification. Dans cette thèse, nous adoptons une approche de la spécification formelle des diagrammes M-UML dans le système Maude. Nous avons appliqué notre approche en trois étapes proposées au diagramme d'états-transitions, l'un des diagrammes les plus importants de M-UML. La technique consiste à dériver systématiquement une description formelle de Maude à partir de ce type d'analyse de diagramme, et nous avons obtenu des résultats très satisfaisants. Cette transcription proposée permet d'obtenir une spécification algébrique exprimée en logique de réécriture. Ce dernier sera utilisé pour vérifier les spécifications des systèmes à base d'agents mobiles.Côte titre : DI/0075 En ligne : http://dspace.univ-setif.dz:8888/jspui/bitstream/123456789/4095/1/Mourad%20Kezai [...] Format de la ressource électronique : Exemplaires
Code-barres Cote Support Localisation Section Disponibilité aucun exemplaire
Titre : Transcription des spécifications M-UML vers le système Maude Type de document : document électronique Auteurs : Mourad kezai, Auteur ; Khababa,Abdellah, Directeur de thèse Année de publication : 2023 Importance : 1 vol (157 f .) Format : 29cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : système Maude
LTL (Linear Time Logic)Index. décimale : 004 Informatique Résumé : Les systèmes multi-agents forment un type intéressant de modélisation de sociétés, car ils ont des domaines d'application très larges. Par conséquent, le domaine de la technologie des "agents mobiles" représente un concept nouveau et important en intelligence artificielle et de l'ingénieries de logiciels. Malgré l'intérêt porté à cette technologie, la plupart des approches à l'heure ne permettent pas une conception suffisante et complète des agents mobiles.
D'autre part, Maude est un environnement de spécification, de programmation orientée objet et de preuve basé sur une logique de réécriture qui est un cadre sémantique unificateur de plusieurs modèles de concurrence. En plus, le système Maude dispose également d'une batterie d'outils permettent la simulation, l’analyse d'accessibilité par le LTL (Linear Time Logic) Model-checker permettant la vérification et le prototypage des propriétés de spécification.
Enfin, la méthode graphique UML généralement et ses extensions permettent de représenter de manière synthétique et intuitive les systèmes multi-gent. Cependant, elles ne sont pas dotées permettant de faire la vérification. Dans cette thèse, nous adoptons une approche de la spécification formelle des diagrammes M-UML dans le système Maude. Nous avons appliqué notre approche en trois étapes proposées au diagramme d'états-transitions, l'un des diagrammes les plus importants de M-UML. La technique consiste à dériver systématiquement une description formelle de Maude à partir de ce type d'analyse de diagramme, et nous avons obtenu des résultats très satisfaisants. Cette transcription proposée permet d'obtenir une spécification algébrique exprimée en logique de réécriture. Ce dernier sera utilisé pour vérifier les spécifications des systèmes à base d'agents mobiles.Côte titre : DI/0075 En ligne : http://dspace.univ-setif.dz:8888/jspui/bitstream/123456789/4095/1/Mourad%20Kezai [...] Format de la ressource électronique : Transcription des spécifications M-UML vers le système Maude [document électronique] / Mourad kezai, Auteur ; Khababa,Abdellah, Directeur de thèse . - 2023 . - 1 vol (157 f .) ; 29cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : système Maude
LTL (Linear Time Logic)Index. décimale : 004 Informatique Résumé : Les systèmes multi-agents forment un type intéressant de modélisation de sociétés, car ils ont des domaines d'application très larges. Par conséquent, le domaine de la technologie des "agents mobiles" représente un concept nouveau et important en intelligence artificielle et de l'ingénieries de logiciels. Malgré l'intérêt porté à cette technologie, la plupart des approches à l'heure ne permettent pas une conception suffisante et complète des agents mobiles.
D'autre part, Maude est un environnement de spécification, de programmation orientée objet et de preuve basé sur une logique de réécriture qui est un cadre sémantique unificateur de plusieurs modèles de concurrence. En plus, le système Maude dispose également d'une batterie d'outils permettent la simulation, l’analyse d'accessibilité par le LTL (Linear Time Logic) Model-checker permettant la vérification et le prototypage des propriétés de spécification.
Enfin, la méthode graphique UML généralement et ses extensions permettent de représenter de manière synthétique et intuitive les systèmes multi-gent. Cependant, elles ne sont pas dotées permettant de faire la vérification. Dans cette thèse, nous adoptons une approche de la spécification formelle des diagrammes M-UML dans le système Maude. Nous avons appliqué notre approche en trois étapes proposées au diagramme d'états-transitions, l'un des diagrammes les plus importants de M-UML. La technique consiste à dériver systématiquement une description formelle de Maude à partir de ce type d'analyse de diagramme, et nous avons obtenu des résultats très satisfaisants. Cette transcription proposée permet d'obtenir une spécification algébrique exprimée en logique de réécriture. Ce dernier sera utilisé pour vérifier les spécifications des systèmes à base d'agents mobiles.Côte titre : DI/0075 En ligne : http://dspace.univ-setif.dz:8888/jspui/bitstream/123456789/4095/1/Mourad%20Kezai [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité DI/0075 DI/0075 Thèse Bibliothéque des sciences Français Disponible
Disponible
