L'Odyssée des Graphes de Diagrammes de Séquences (MSC-Graphes)

Sujets

• Processus cognitifs
• Formule brute
• D'une ombre à l'autre
• Msuata
• Boucles d'or et les Trois Ours
• Relation de un à un

Informations

• Publié par: Asla
• Nombre de lectures: 145
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

Université Paris 7 - Denis Diderot – UFR d’informatique – Année 2004 Thèse pour l’obtention du diplôme de docteur de l’université Paris 7, spécialité informatique présentée par Blaise GENEST le 29 Novembre 2004 L’Odyssée des Graphes de Diagrammes de Séquences (MSC-Graphes) soutenue publiquement devant le jury suivant : Paul Gastin Examinateur Claude Jard Rapporteur Anca Muscholl Directrice de thèse Philippe Schnœbelen Président du Jury P.S. Thiagarajan Rapporteur Igor Walukiewicz Rapporteur2Remerciements Je tiens tout d’abord à remercier Anca, bien plus qu’une directrice de Thèse. Pour ses conseils, sa patience, son enthousiasme. Sa gentillesse aussi. Tout ce qu’elle m’a appris enfin. Et puis pour les noms imaginatifs et amu sants des macros et autres labels que personne ne verra jamais dans les papiers que nous avons écrit (et écrirons) ensemble. MerciensuiteàPhilippeSchnœbelenpouravoiracceptéd’êtreleprésident du jury. Cette thèse serait sans doute différente sans ce qu’il m’a appris lors d’un stage sous sa (co)direction ("ce que tu as fait ne sera pas perdu" avait il alorsditavecprémonition).MesremerciementsvontégalementàPaulGastin pouraccepter de participer au jury, maisaussi pour sesexposés fréquents qui m’ont permis de mieux appréhender les logiques temporelles (concurrentes). J’aihonteusement recopié danslabibliographie ([DG04])unde sesabstracts, mais comment faire autrement vu la limpidité de la description? Je dois aussi beaucoup aux membres de la défunte ARC FISC, les parte nairesfrancaisdechoixconcernant lesscénarios. Jepense notamentàClaude Jard pour avoir accepté la lourde tâche de rapporter cette thèse. Merci aussi aux membres bordelais des nombreuses ACI nous liant, en particulier Igor Walukiewicz, qui a dù se battre avec mon francais en acceptant d’être rap porteur. Enfin, P.S. Thiagarajan a eu la gentillesse de faire un rapport sur la thèse, et je lui en suis reconnaissant. Le lecteur attentif aura sans doute déjà compris que j’accorde un place importante à toutes les personnes avec lesquelles j’ai travaillé pendant ses années de thèse, qu’il y ait eu ou non un article écrit à la clef. Pour moi, c’est cette coopération qui forme la recherche. Je souhaite les remercier tous collectivement ici, la liste serait trop longue et je risquerais d’en oublier. Merci enfin à Jack Allgood (ou pas), sans qui cette thèse ne serait pas en Français. Enfin, je souhaite remercier les amis du Liafa, de Cachan et d’ailleurs, qui m’ont supporté pendant cette période. 34Table des matières I Automates, Communication et Diagrammes. 15 1 Structures Multiples 17 1.1 Langages Réguliers . . . . . . . . . . . . . . . . . . . . . . . . 17 1.1.1 Un Modèle de Machines . . . . . . . . . . . . . . . . . 18 1.1.2 Représentations Différentes . . . . . . . . . . . . . . . 21 1.2 Machines de Turing . . . . . . . . . . . . . . . . . . . . . . . . 24 1.2.1 Définition . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.2.2 Décidabilité et Complexité . . . . . . . . . . . . . . . . 25 1.3 Traces de Mazurkiewicz . . . . . . . . . . . . . . . . . . . . . 29 1.3.1 Langages Réguliers et Rationnels . . . . . . . . . . . . 31 1.3.2 Théorème d’Ochmański . . . . . . . . . . . . . . . . . . 33 1.3.3 Traces et Communication . . . . . . . . . . . . . . . . 40 1.4 Automates Communicants . . . . . . . . . . . . . . . . . . . . 42 1.4.1 Diagrammes de Séquences (MSC) . . . . . . . . . . . . 48 1.4.2 Autres Représentations de la Communication . . . . . 52 1.5 MSC graphes . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 2 Extension du Théorème de Kleene-Büchi 63 2.1 MSC graphes et CFM . . . . . . . . . . . . . . . . . . . . . . 64 2.1.1 CMSC Graphes . . . . . . . . . . . . . . . . . . . . . . 64 2.1.2 Un Modèle Général . . . . . . . . . . . . . . . . . . . . 68 2.2 Borne Existentielle . . . . . . . . . . . . . . . . . . . . . . . . 70 2.3 Coopération des Processus . . . . . . . . . . . . . . . . . . . . 74 2.3.1 L’Alphabet de Kuske . . . . . . . . . . . . . . . . . . . 77 2.3.2 CMSC Graphes Réguliers . . . . . . . . . . . . . . . . 82 2.4 Le Théorème Central . . . . . . . . . . . . . . . . . . . . . . . 84 2.4.1 De MSO à un ensemble régulier de représentants . . . 84 2.4.2 Théorème de Zielonka . . . . . . . . . . . . . . . . . . 86 5TABLE DES MATIÈRES TABLE DES MATIÈRES 2.4.3 Un CFM proche d’une application asynchrone . . . . . 87 2.4.4 Les τ Cycles . . . . . . . . . . . . . . . . . . . . . . . . 90 b 2.4.5 Un CFM qui reconnaîtMSC . . . . . . . . . . . . . . 93 2.5 Voir plus loin? . . . . . . . . . . . . . . . . . . . . . . . . . . 95 II Vérification 99 3 Implémentation 101 3.1 MSC Graphes à Choix Local . . . . . . . . . . . . . . . . . . . 102 3.1.1 Définition . . . . . . . . . . . . . . . . . . . . . . . . . 102 3.1.2 Des Protocoles Concrets . . . . . . . . . . . . . . . . . 106 3.2 Expressivité . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 3.2.1 Caractérisation des MSC graphes à Choix Local . . . . 109 3.2.2 Deux Algorithmes de Test . . . . . . . . . . . . . . . . 114 3.3 Voir plus loin? . . . . . . . . . . . . . . . . . . . . . . . . . . 119 4 Model-Checking 121 4.1 Logiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 4.2 MSC Graphes . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 4.2.1 Appartenance (Membership) . . . . . . . . . . . . . . . 123 4.2.2 Model Checking . . . . . . . . . . . . . . . . . . . . . . 125 4.2.3 MSC Graphes à Choix Local . . . . . . . . . . . . . . . 126 4.3 Template MSC . . . . . . . . . . . . . . . . . . . . . . . . . . 133 4.3.1 Expressivité . . . . . . . . . . . . . . . . . . . . . . . . 138 4.3.2 Model checking . . . . . . . . . . . . . . . . . . . . . . 140 4.4 Voir plus loin? . . . . . . . . . . . . . . . . . . . . . . . . . . 149 5 Heuristiques pour Réduire la Taille des Modèles 151 5.1 Projection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 5.1.1 Projections et Sûreté . . . . . . . . . . . . . . . . . . . 153 5.1.2 Caractérisation des MSC graphes . . . . . . . . . . . . 159 5.1.3 Les Atomes sont Réguliers . . . . . . . . . . . . . . . . 162 5.2 Compression . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 5.2.1 Syntaxe et Sémantique des nested MSC. . . . . . . . . 170 5.2.2 Reconnaissance de Motifs . . . . . . . . . . . . . . . . 173 5.2.3 Le Problème d’Appartenance . . . . . . . . . . . . . . 181 5.3 Voir plus loin? . . . . . . . . . . . . . . . . . . . . . . . . . . 188 6Introduction Les Enjeux Les protocoles de communication sont des règles d’échange entre plu sieurs processus, plus ou moins proches. Avec le développement des réseaux de communication, telsInternet et les réseaux de téléphonie (mobile ou non), la complexité des protocoles mis en jeux s’accroît de manière vertigineuse. De même, la miniaturisation des composants électroniques permet d’intégrer dans la même puce de plus en plus de possibilités, concrétisées par des proto coles de communication nombreux et constamment mis à jour. Par exemple, les transactions sur internet sont régies par des protocoles bien précis. De même, dans un ordinateur, un contrôleur mémoire accède aux données sto ckées d’une manière très spéciale. Les communications se séparent en deux grandes catégories : – Synchrones lorsque les données s’échangent entre les différents proces sus à des instants bien déterminés (les tops d’horloge). La grande spé cificité de ces échanges est que le temps pour communiquer une donnée précise d’un processus à un autre est connu. Ce type de communica tion ne peut être mis en œuvre que si la topologie exacte du réseau est connue, les canaux de communication sûrs et de débit constant, par exemple à l’intérieur d’un processeur. De plus, la vitesse de communi cation est décidée par le processus le plus lent. – Asynchroneslorsque lesdonnées s’échangent entre lesdifférents proces sus lorsque ceux ci sont prêts à les envoyer. Le temps de transmission d’un message ne peut alors pas être connu a priori. Ce type de commu nication peut être mis plus facilement en œuvre. La seconde catégorie de communication semble prendre le pas sur le pre mière à cause de sa simplicité à mettre en œuvre et de sa meilleure perfor mance. Nous nous intéresserons ainsi à cette seconde catégorie de communication. Nous choisirons également d’étudier les communications asynchrones par passage de messages, plutôt que par variables partagées. Comprendre. Le grand problème des protocoles asynchrones est qu’ils sont intrinsèquement plus compliqués à comprendre que les protocoles syn 1chrones . Ainsi, une des premières tâches est de comprendre quel genre de protocole il est possible de décrire avec quel genre de structure. Ce travail +a été commencé dans [HMNK 04] pour des protocoles restreints, puis repris par [Kus03, Mor02]. Dernièrement, [BL04] ont obtenu des résultats partiels sans restriction sur les protocoles. Construire. En fait, les protocoles de communication mettent en œuvre des processus en parallèle, c’est à dire faisant des choix dépendant unique ment de leur connaissance, et non de la connaissance de l’état des autres processus. Nous dirons de tels protocoles qu’ils sont à contrôle local. Une croyance partagée par beaucoup est que notre mode de pensée est intrinsè quement séquentielle, et que penser d’une manière parallèle est plus compli qué. Ainsi, un autre but est d’aider à construire des protocoles de commu nication, par exemple en distribuant automatiquement des algorithmes trop séquentiels en des algorithmes avec un contrôle local, comme l’ont commencé [AEY00, AEY01, BM03] en supposant qu’il ne pouvait y avoir des données additionnelles de contrôle. Une approche différente a été menée par [HJ00] en exhibant une classe de langages toujours implantable, et par [CDHL00] qui supposaient que plus de libertés étaient laissées aux ingénieurs. Vérifier. Enfin, la complexité grandissante des protocoles de communi cation a amené à de nombreuses erreurs par le passé. Tous les protocoles de communicati