Modelisation Des Structures D Echanges De Donnees Dans Un Environnement Parallele Approche Par Simulation A Evenements Discrets

MODELISATION DES STRUCTURES D'ECHANGES DE DONNEES DANS UN ENVIRONNEMENT PARALLELE

L'ANALYSE DES PERFORMANCES DES MACHINES MULTIPROCESSEURS PEUT S'ENVISAGER DE PLUSIEURS MANIERES: L'APPROCHE ANALYTIQUE, L'UTILISATION DE LOGICIELS DE SIMULATION SPECIFIQUES OU L'UTILISATION DE SIMULATEURS EXISTANTS ET D'APPLICATION TRES GENERALE. LA SIMULATION A EVENEMENTS DISCRETS AVEC LE SIMULATEUR SIMAN A ETE RETENUE. AINSI LES PRINCIPAUX ELEMENTS DU SYSTEME SONT MODELISES SANS ATTEINDRE LE NIVEAU ELECTRONIQUE DU COMPOSANT. AFIN DE VALIDER NOTRE APPROCHE, NOUS AVONS EFFECTUE UNE ETUDE COMPAREE, ENTRE L'APPROCHE ANALYTIQUE ET LA MODELISATION PAR SIMAN, DU PROBLEME DE LA COHERENCE ENTRE LES CACHES. LES RESULTATS OBTENUS MONTRENT QUE NOTRE APPROCHE EST PRECISE ET SENSIBLE. DE PLUS, NOUS AVONS MIS EN EVIDENCE SES APPORTS PAR RAPPORT A LA SOLUTION ANALYTIQUE. AFIN DE MONTRER L'INTERET DE L'APPROCHE, UN CAS PRATIQUE EST ETUDIE: UN SYSTEME CIBLE A TROIS TRANSPUTERS. LES RESULTATS COMPARES ENTRE LES SIMULATIONS D'UN PROGRAMME REEL SUR LE MODELE DU SYSTEME ET L'EXECUTION REELLE CONFIRMENT L'EXACTITUDE ET LA PRECISION DE NOTRE METHODE D'ANALYSE DU COMPORTEMENT DU SYSTEME CIBLE. BIEN QUE L'ETUDE AIT ETE EFFECTUEE SUR UNE MACHINE A BASE DE TROIS TRANSPUTERS, ELLE PEUT SANS DIFFICULTES ETRE APPLIQUEE A DES ARCHITECTURES PLUS COMPLEXES

Modelisation des structures d'echanges de donnees dans un environnement parallele : approche par simulation a evenements discrets

De la modélisation formelle à la simulation à évènements discrets

La conception de protocoles de communication repose généralement sur des modèles fonctionnels élaborés à partir des besoins du système.Dans les systèmes de transport intelligents (ITS), les fonctionnalités étudiées incluent l'auto-organisation, le routage, la fiabilité, la qualité de service et la sécurité. Les évaluations par simulation sur les protocoles dédiés aux ITS se focalisent sur les performances dans des scénarios spécifiques. Or, l'évolution des transports vers les véhicules autonomes nécessite des protocoles robustes offrant des garanties sur certaines de leurs propriétés. Les approches formelles permettent de fournir la preuve automatique de certaines propriétés, mais pour d'autres il est nécessaire de recourir à une preuve interactive impliquant le savoir d'un Expert. Les travaux menés dans cette thèse poursuivent l'objectif d'élaborer, dans le formalisme DEVS (Discrete Event System Specification), des modèles d'un ITS dont la simulation permettrait d'observer les propriétés, éventuellement vérifiées par une approche formelle, dans un scénario plus large et de générer sur les modèles des données susceptibles d'alimenter une boucle de preuve interactive au lieu d'un Expert. Prenant pour cible le protocole CBL-OLSR (Chain-Branch- Leaf inOptimized Link State Routing), cette thèse montre comment un modèle DEVS et un modèle formel Event-B équivalents peuvent être construits à partir de la même spécification fonctionnelle d'un réseau ad hoc où les nœuds utilisent ce protocole. Des propriétés relatives à la sûreté et à la sécurité sont introduites dans le modèle formel Event-B afin d'être vérifiées, puis une méthodologie est proposée afin de les transférer dans un modèle DEVS équivalent sous forme de contraintes, de choix ou d'observables selon des critères proposés. Enfin, cette thèse ouvre également les perspectives de l'automatisation de ce processus de conception, de l'intégration à la simulation DEVS de données réelles à la fois sur le trafic routier et sur les flux d'applications dédiées aux véhicules, et de l'interaction avec des simulateurs spécialisés pour les différents composants (par exemple MATLAB pour les modèles de propagation, OPNET ou NS3 pour les communications, SUMO pour les modèles de mobilité) ; le but étant une évaluation du protocole dans un contexte très réaliste du système.