Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

REPUBLIQUE TUNISIENNE MINISTERE DE L’ENSEIGNEMENT SUPERIEUR, DE LA RECHERCHE SC

REPUBLIQUE TUNISIENNE MINISTERE DE L’ENSEIGNEMENT SUPERIEUR, DE LA RECHERCHE SCIENTIFIQUE ET DE LA TECHNOLOGIE UNIVERSITE DE MONASTIR FACULTE DES SCIENCES DE MONASTIR MEMOIRE Présenté pour l’obtention du diplôme de : MASTERE Spécialité : INFORMATIQUE Par : Mohamed GAROUI Sujet : Vers une Approche de Spécification Formelle des Systèmes Multi-Agents Holoniques Soutenu le 24 Septembre 2011, devant le jury composé : Dr. Nazih OMRI Président Maître de Conférences FSM Dr. Mohamed GRAIET Rapporteur Maître Assistant ISIMM Dr. Belhassen MAZIGH Encadreur Maître Assistant, FSM Laboratoire ……………………… (Code : MESRST ……/UR/LR…………….) N° d’ordre : 1 Mémoire de Master DISCIPLINE : INFORMATIQUE Vers une approche de Spécification formelle des systèmes Multi-Agents Holoniques Par Mohamed GAROUI Encadré par : Belhassen MAZIGH 2 Table des matières CHAPITRE 1 INTRODUCTION ...................................................................................................................................... 9 1.1 Contexte .................................................................................................................................. 9 1.2 Première analyse et objectifs de ces travaux ....................................................................... 9 1.3 Etat de l’art .......................................................................................................................... 10 1.3.1 Les Méthodes formelles ............................................................................................... 10 1.3.2 La spécification formelle ............................................................................................. 10 1.3.3 Les preuves formelles .................................................................................................. 10 1.3.4 Les systèmes Multi-Agents .......................................................................................... 11 1.3.5 Les systèmes Multi-Agents Holoniques ......................................................................... 12 1.3.6 Le méta modèle CRIO (Capacité, Rôle, Interaction, Organisation) ........................... 14 1.3.7 Le Processus ASPECS (Agent-oriented Software Process for Engineering Complex Systems) 14 CHAPITRE 2 LANGAGES FORMELS ........................................................................................................................... 18 2.1 Introduction ......................................................................................................................... 18 2.2 Systèmes formels, vérification, preuve, model-checking .................................................. 18 2.3 Quelques langages formels.................................................................................................. 19 2.3.1 Z et Object-Z ................................................................................................................ 19 2.3.2 La méthode B ............................................................................................................... 21 2.3.3 Les réseaux de Petri..................................................................................................... 22 2.4 Conclusion ............................................................................................................................ 23 CHAPITRE 3 DEUX FORMALISMES COMPLEMENTAIRES : LES RESEAUX DE PETRI ET OBJECT-Z ...................... 25 3.1 Introduction ......................................................................................................................... 25 3.2 Les réseaux de Petri ............................................................................................................ 25 3.2.1 Concepts propres aux réseaux de Petri ..................................................................... 26 3.2.2 Concepts et définitions ................................................................................................ 26 3.2.3 Propriétés usuelles ....................................................................................................... 28 3.2.4 Sémantique des Réseaux de Petri ............................................................................... 29 3.3 Le langage Object-Z ............................................................................................................ 29 3.3.1 La Syntaxe d’Object-Z ................................................................................................ 30 3 3.3.2 Sémantique de trace et invariants temporels ............................................................ 33 3.4 Conclusion ............................................................................................................................ 34 CHAPITRE 4 METHODE DE COMPOSITION DES SPECIFICATIONS PARTIELLES .................................................... 35 4.1 Introduction ......................................................................................................................... 35 4.2 Aperçu de notre approche .................................................................................................. 35 4.3 Intégration syntaxique ........................................................................................................ 36 4.3.1 Principes ....................................................................................................................... 36 4.3.2 Aspects des RdP exprimés en Object-Z ..................................................................... 36 4.4 Règles de traduction du RdP vers le domaine syntaxique partagé ................................. 45 4.4.1 Définition de la fonction Y Y Y Y .......................................................................................... 45 4.5 Intégration sémantique ....................................................................................................... 46 4.5.1 Aperçu .......................................................................................................................... 46 4.5.2 Système de transitions ................................................................................................. 46 4.5.3 Système de transitions temporisées ............................................................................ 47 4.5.4 Technique de transformation ..................................................................................... 48 4.5.4.1 De la classe Object-Z à un système de transitions .................................................... 48 i. Exemple : classe Object-Z simpletrans....................................................................... 49 4.1 Exemple d’intégration complète ........................................................................................ 55 4.3 Conclusion ............................................................................................................................ 62 CHAPITRE 5 APPROCHE DE SPECIFICATION FORMELLE D’UN SYSTEME MULTI-AGENT HOLONIQUE ............... 64 5.1 Introduction ......................................................................................................................... 64 5.2 Domaine du Problème associé au méta-modèle CRIO ..................................................... 64 5.2.1 Spécification ................................................................................................................. 64 5.2.2 Lemmes ......................................................................................................................... 67 5.2.3 Exemple ........................................................................................................................ 67 5.3 Domaine d’agentification associé au méta-modèle CRIO ................................................ 75 5.3.1 Spécification ................................................................................................................. 75 5.3.2 Lemmes ......................................................................................................................... 80 5.3.3 Exemple ........................................................................................................................ 81 5.4 Génération semi-automatique des instances à partir de la spécification ........................ 85 5.4.1 Exemple ........................................................................................................................ 86 5.5 Conclusion ............................................................................................................................ 88 4 CHAPITRE 6 VERIFICATION DE SPECIFICATION DE SYSTEMES MULTI-AGENTS HOLONIQUE : CAS DE L’ENTREPRISE DE FABRICATION DES AUTOMOBILES PEUGEOT .................................................... 90 6.1 Introduction ......................................................................................................................... 90 6.2 Présentation du système ...................................................................................................... 90 6.3 Modélisation ......................................................................................................................... 91 6.3.1 Domaine du Problème ................................................................................................. 91 6.3.2 Domaine d’agentification ............................................................................................ 93 6.4 Spécification ......................................................................................................................... 93 6.4.1 Domaine du Problème ................................................................................................ 93 6.4.2 Domaine d’agentification ............................................................................................ 99 6.5 Vérification ......................................................................................................................... 103 6.5.1 Définition des états du système de transitions ......................................................... 104 6.5.2 Définition des transitions du système de transition ................................................ 104 6.5.3 Preuve ......................................................................................................................... 105 6.6 Implémentation sur la plateforme Janus ........................................................................ 105 6.6.1 Plateforme Janus ....................................................................................................... 105 6.6.2 Exemple ...................................................................................................................... 105 6.7 Conclusion .......................................................................................................................... 111 CONCLUSION ...................................................................................................................................... 113 Annexes .............................................................................................................................................. 115 ANNEXE A FRAMEWORK SAL (SYMBOLIC ANALYSIS LABORATORY) ............................................................. 116 BIBLIOGRAPHIE .................................................................................................................................. 121 5 Table des figures Fig. 1 : Un holon composé de trois holons membres ............................................................................ 12 Fig. 2: Structure Holonique (ﬁgure inspirée de [Ferber, 1995, p. 100]) ................................................ 13 Fig. 3 : Modèle du Réseau de Petri........................................................................................................ 26 Fig. 4 : Syntaxe d’une classe Object-Z .................................................................................................. 30 Fig. 5 : Schéma Object-Z du classe CreditCard .................................................................................... 31 Fig. 6 : Réseau de Petri Ordinaire ......................................................................................................... 37 Fig. 7 : Spécification d’un RdP ordinaire basée sur la syntaxe de classe OZ........................................ 38 Fig. 8 : Réseau de Petri généralisé......................................................................................................... 39 Fig. 9 : Spécification d’un RdP généralisé basée sur la syntaxe de classe OZ ...................................... 40 Fig. 10 : Exemple de Réseau de Petri à arc inhibiteur .......................................................................... 40 Fig. 11 : Spécification d’un RdP à arcs inhibiteurs basée sur la syntaxe de classe OZ ......................... 41 Fig. 12 : Réseau de Petri à capacité ....................................................................................................... 42 Fig. 13 : Spécification d’un RdP à capacité basée sur la syntaxe de classe OZ .................................... 42 Fig. 14 : Spécification d’un RdP temporise basée sur la syntaxe de classe OZ .................................... 43 Fig. 15 : Réseau de Petri Temporel ....................................................................................................... 44 Fig. 16 : Spécification d’un RdP Temporel basée sur la syntaxe de classe OZ .................................... 45 Fig. 17 : les éléments d’une classe Object-Z ......................................................................................... 49 Fig. 18 : Classe Object-Z "simpletrans" ................................................................................................ 50 Fig. 19 : Fichier SAL relatif à la classe Object-Z "simpletrans" ........................................................... 53 Fig. 20 : Réseau de Petri pour le système d’interrupteur....................................................................... 54 Fig. 21: Fichier SAL relatif au réseau de Petri du système "interrupteur" ........................................... 55 Fig. 22 : Spécification du système Key basée sur la syntaxe PNOZ .................................................... 56 Fig. 23 : Spécification du système Lock basée sur la syntaxe PNOZ .................................................... 57 Fig. 24 : Spécification du système Door basée sur la syntaxe PNOZ .................................................. 58 Fig. 25 : Spécification du système KeySystem basée sur la syntaxe PNOZ .......................................... 59 Fig. 26 : Classe Capacity basée sur la syntaxe PNOZ.......................................................................... 65 Fig. 27 : Classe Role basée sur la syntaxe PNOZ ................................................................................. 65 Fig. 28 : Classe Interaction basée sur la syntaxe PNOZ ...................................................................... 66 Fig. 29 : Classe Organisation basée sur la syntaxe PNOZ ................................................................... 67 Fig. 30: Description de l’organisation du simulateur des robots footballeurs ....................................... 68 Fig. 31 : Classe PlayersSimulatorRole basée sur la syntaxe PNOZ ..................................................... 69 Fig. 32 : Classe RoleAssignerRole basée sur la syntaxe PNOZ ........................................................... 70 Fig. 33 : Classe StrategySelectorRole basée sur la syntaxe PNOZ ...................................................... 71 Fig. 34 : Classe GameObserverRole basée sur la syntaxe PNOZ ........................................................ 72 Fig. 35 : Classe AssociateTacticalRoleAndPlayer Interaction basée sur la syntaxe PNOZ ................. 73 Fig. 36 : Classe AssignsStrategy Interaction basée sur la syntaxe PNOZ ............................................ 73 Fig. 37 : Classe ProvidesPlayersPositions Interaction basée sur la syntaxe PNOZ ............................. 73 Fig. 38 : Classe PlayStrategy Capacité basée sur la syntaxe PNOZ .................................................... 74 Fig. 39 : Classe ObserveGame Capacité basée sur la syntaxe PNOZ .................................................. 74 Fig. 40 : Classe ChooseStrategy Capacité basée sur la syntaxe PNOZ ............................................... 74 Fig. 41 : Classe TeamSimulation Organisation basée sur la syntaxe PNOZ ........................................ 75 Fig. 42 : Classe AgentTask basée sur la syntaxe PNOZ ....................................................................... 75 6 Fig. 43 : Classe Service basée sur la syntaxe PNOZ ............................................................................ 76 Fig. 44 : Classe AgentRole basée sur la syntaxe PNOZ ....................................................................... 76 Fig. 45 : Classe Goal basée sur la syntaxe PNOZ ................................................................................ 76 Fig. 46 : Classe IndividualGoal basée sur la syntaxe PNOZ ................................................................ 77 Fig. 47 : Classe CollectiveGoal basée sur la syntaxe PNOZ ................................................................ 77 Fig. 48 : Classe AutonomousEntity basée sur la syntaxe PNOZ .......................................................... 77 Fig. 49 : Classe Agent basée sur la syntaxe PNOZ ............................................................................... 78 Fig. 50 : Classe HolonicRole basée sur la syntaxe PNOZ .................................................................... 78 Fig. 51 : Classe HolonicMember basée sur la syntaxe PNOZ .............................................................. 78 Fig. 52 : Classe Group basée sur la syntaxe PNOZ ............................................................................. 79 Fig. 53 : Classe HolonicGroup basée sur la syntaxe PNOZ ................................................................. 79 Fig. 54 : Classe ProductionGroup basée sur la syntaxe PNOZ ............................................................ 79 Fig. 55 : Classe Holon basée sur la syntaxe PNOZ .............................................................................. 80 Fig. 56: La structure holonique du simulateur de robots footballeurs ................................................... 81 Fig. 57 : Classe Holon H1 basée sur la syntaxe PNOZ ........................................................................ 82 Fig. 58 : Classe Holon H2 basée sur la syntaxe PNOZ ........................................................................ 82 Fig. 59 : Classe Membre holonique H3 basée sur la syntaxe PNOZ .................................................... 82 Fig. 60 : Classe Holon H3 basée sur la syntaxe PNOZ ........................................................................ 83 Fig. 61 : Classe PlayersSimulator AgentRole basée sur la syntaxe PNOZ .......................................... 83 Fig. 62 : Classe Groupe Holonique g3 basée sur la syntaxe PNOZ ..................................................... 84 Fig. 63 : Classe Groupe Productive g4 basée sur la syntaxe PNOZ ..................................................... 84 Fig. 64 : Classe Agent H11 basée sur la syntaxe PNOZ ...................................................................... 84 Fig. 65 : Classe Interaction TeamToTeam basée sur la syntaxe PNOZ ................................................ 85 Fig. 66 : Classe Groupe GameSimulation basée sur la syntaxe PNOZ ................................................ 85 Fig. 67 : Instanciation du fichier XML à partir du fichier XML schéma .............................................. 86 Fig. 68 : XML schéma du domaine uploads/s3/ memo-fsm.pdf