Remerciez-le!

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

Memo fsm N d ? ordre 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éciali

N d ? ordre 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éci ?cation Formelle des Systèmes Multi-Agents Holoniques Soutenu le Septembre devant le jury composé Dr Nazih OMRI Dr Mohamed GRAIET Dr Belhassen MAZIGH Président Rapporteur Encadreur Ma? tre de Conférences FSM Ma? tre Assistant ISIMM Ma? tre Assistant FSM Laboratoire ? ? ? ? ? ? ? ? ? Code MESRST ? ? UR LR ? ? ? ? ? CMémoire de Master DISCIPLINE INFORMATIQUE Vers une approche de Spéci ?cation formelle des systèmes Multi-Agents Holoniques Par Mohamed GAROUI Encadré par Belhassen MAZIGH CTable des matières CHAPITRE INTRODUCTION Contexte Première analyse et objectifs de ces travaux Etat de l ? art Les Méthodes formelles La spéci ?cation formelle Les preuves formelles Les systèmes Multi- Agents Les systèmes Multi-Agents Holoniques Le méta modèle CRIO Capacité Rôle Interaction Organisation Le Processus ASPECS Agent-oriented Software Process for Engineering Complex Systems CHAPITRE LANGAGES FORMELS Introduction Systèmes formels véri ?cation preuve model- checking Quelques langages formels Z et Object- Z La méthode B Les réseaux de Petri Conclusion CHAPITRE DEUX FORMALISMES COMPLEMENTAIRES LES RESEAUX DE PETRI ET OBJECT-Z Introduction Les réseaux de Petri Concepts propres aux réseaux de Petri Concepts et dé ?nitions Propriétés usuelles Sémantique des Réseaux de Petri Le langage Object-Z La Syntaxe d ? Object- Z C Sémantique de trace et invariants temporels Conclusion CHAPITRE METHODE DE COMPOSITION DES SPECIFICATIONS PARTIELLES Introduction Aperçu de notre approche Intégration syntaxique Principes Aspects des RdP exprimés en Object-Z Règles de traduction du RdP vers le domaine syntaxique partagé Dé ?nition de la fonction Y Intégration sémantique Aperçu Système de transitions Système de transitions temporisées Technique de transformation De la classe Object-Z à un système de transitions i Exemple classe Object-Z simpletrans Exemple d ? intégration complète Conclusion CHAPITRE APPROCHE DE SPECIFICATION FORMELLE D ? UN SYSTEME MULTI- AGENT HOLONIQUE Introduction Domaine du Problème associé au méta-modèle CRIO Spéci ?cation Lemmes Exemple Domaine d ? agenti ?cation associé au méta-modèle CRIO Spéci ?cation Lemmes Exemple Génération semi-automatique des instances à partir de la spéci ?cation Exemple Conclusion CCHAPITRE VERIFICATION DE SPECIFICATION DE SYSTEMES MULTI- AGENTS HOLONIQUE CAS DE L ? ENTREPRISE DE FABRICATION DES AUTOMOBILES PEUGEOT Introduction Présentation du système Modélisation Domaine du Problème Domaine d ? agenti ?cation Spéci ?cation Domaine du Problème Domaine d ? agenti ?cation Véri ?cation Dé ?nition des états du système de transitions Dé ?nition des transitions du système de transition Preuve Implémentation sur la plateforme Janus Plateforme Janus Exemple Conclusion CONCLUSION Annexes ANNEXE A FRAMEWORK SAL SYMBOLIC ANALYSIS LABORATORY BIBLIOGRAPHIE CTable des ?gures Fig Un holon composé de trois holons membres Fig Structure Holonique ?gure inspirée de Ferber p Fig Modèle du Réseau de Petri Fig Syntaxe d ? une classe Object- Z Fig Schéma Object-Z du classe CreditCard Fig Réseau