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 Rapporteur2Remerciements 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 ...
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 Rapporteur2Remerciements
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.
34Table 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
5TABLE 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
6Introduction
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 communication. 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