these

Description

UNIVERSIT DE NICE - SOPHIA ANTIPOLIS UFR Sciences cole Doctorale STICTH¨SEpour obtenir le titre deDocteur en Sciencesde l’UniversitØ de Nice - Sophia AntipolisSpØcialitØ : InformatiqueprØsentØe et soutenue parRabØa Ameur-Boulifa quip e d’accueil : OASIS INRIA Sophia-Antipolis - CNRS - I3S - UNSAGØnØration de modŁles comportementaux desapplications rØpartiesThŁse dirigØe par Eric MadelainePrØsentØe publiquement le mercredi 15 dØcembre 2004devant le jury composØ de :PrØsident Jean-Paul Rigault UniversitØ, Nice-Sophia AntipolisRapporteurs : Fran ois Vernadat INSA, ToulouseAlessandro Fantechi UniversitØ de FlorenceExaminateurs : Thomas Jensen IRISA, RennesRadu Mateescu INRIA, Rh ne-Alp esDirecteur de thŁse : Eric Madelaine Sophia-AntipolisGØnØration de modŁlesdes applications rØpartiesThŁse de doctoratRabØa Ameur-BoulifaDØcembre 2004RemerciementsJe tiens à remercier Alessandro Fantechi et Fran ois Vernadat d’avoir acceptØla t che dØlicate d’Œtre rapporteurs, Jean-Paul Rigault, Thomas Jensen et Radu Ma-teescu d’avoir bien voulu m’accorder de leur temps en faisant partie du Jury.Eric Madelaine dont j’ai pu apprØcier durant ces annØes de thŁse les grandes qua-litØs humaines et scienti ques, la disponibilitØ malgrØ des activitØs dØbordantes, illustreparfaitement celles-ci.Je remercie Øgalement tous les membres de mon Øquipe d’accueil (OASIS) avec les-quels j’ai passØ trois annØes riches et agrØables. Je pense particuliŁrement à Isabelle ...

Informations

• Publié par: Difef
• Nombre de lectures: 34
• Langue: Français

Extrait

UNIVERSIT DE NICE - SOPHIA ANTIPOLIS UFR Sciences
cole Doctorale STIC
TH¨SE
pour obtenir le titre de
Docteur en Sciences
de l’UniversitØ de Nice - Sophia Antipolis
SpØcialitØ : Informatique
prØsentØe et soutenue par
RabØa Ameur-Boulifa
quip e d’accueil : OASIS INRIA Sophia-Antipolis - CNRS - I3S - UNSA
GØnØration de modŁles comportementaux des
applications rØparties
ThŁse dirigØe par Eric Madelaine
PrØsentØe publiquement le mercredi 15 dØcembre 2004
devant le jury composØ de :
PrØsident Jean-Paul Rigault UniversitØ, Nice-Sophia Antipolis
Rapporteurs : Fran ois Vernadat INSA, Toulouse
Alessandro Fantechi UniversitØ de Florence
Examinateurs : Thomas Jensen IRISA, Rennes
Radu Mateescu INRIA, Rh ne-Alp es
Directeur de thŁse : Eric Madelaine Sophia-AntipolisGØnØration de modŁles
des applications rØparties
ThŁse de doctorat
RabØa Ameur-Boulifa
DØcembre 2004Remerciements
Je tiens ? remercier Alessandro Fantechi et Fran ois Vernadat d’avoir acceptØ
la t che dØlicate d’Œtre rapporteurs, Jean-Paul Rigault, Thomas Jensen et Radu Ma-
teescu d’avoir bien voulu m’accorder de leur temps en faisant partie du Jury.
Eric Madelaine dont j’ai pu apprØcier durant ces annØes de thŁse les grandes qua-
litØs humaines et scienti ques, la disponibilitØ malgrØ des activitØs dØbordantes, illustre
parfaitement celles-ci.
Je remercie Øgalement tous les membres de mon Øquipe d’accueil (OASIS) avec les-
quels j’ai passØ trois annØes riches et agrØables. Je pense particuliŁrement ? Isabelle Attali
pour l’Ønergie dØployØe pour crØer une atmosphŁre de travail accueillante, pour ses auto-
risations et ses relectures ; je pense Øgalement ? Fran oise Baude et Bernard Serpette
pour leurs relectures et leurs conseils. Que le personnel de l’INRIA trouve ici l’expression
de ma reconnaissance.
J’estime tout le long de mes Øtudes avoir eu beaucoup de chance dans les personnes
que j’ai rencontrØ. Je leur dois ØnormØment. Il semblera peut-Œtre fastidieux au lecteur de
les ØnumØrer mais ils s’y reconna tr ont.
Mes plus vifs remerciements ? mes parents et ma famille. Je ne leur serai probable-
ment jamais assez reconnaissante de m’avoir soutenu tout au long de mes Øtudes et d’avoir
supportØ mon dØpart si loin d’eux.
Plus prŁs de moi il y a Amar dont la tendresse et la patience m’a apportØ la moti-
vation nØcessaire ? aller jusqu’au bout et pour qui un simple merci ne su r a jamais.Table des matiŁres
Introduction 3
1 tat de l’art 1
1.1 SØmantique Formelle de Java et applications rØparties . . . . . . . . . . . . 2
1.2 ModŁles comportementaux des parallŁles . . . . . . . . . . . . . 3
1.2.1 GØnØration de modŁles . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.2.2 ModŁles paramØtrØs . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2.3 SystŁmes de transitions . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 VØri cation de modŁles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3.1 Plate-forme d’analyse et vØri cation de programmes . . . . . . . . . 7
1.3.2 Outils de vØri cation . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2 BibliothŁque ProActive 11
2.1 ModŁles de programmation . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1.1 Objet Actif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1.2 CrØation d’objets actifs . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.1.3 Communication entre objets actifs . . . . . . . . . . . . . . . . . . . 14
2.2 Asynchronisme et Futurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Service et Queue de RequŒtes . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.4 Bilan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3 ModŁles comportementaux d’applications nis 19
78 TABLE DES MATI¨RES
3.1 ModŁles Comportementaux . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.1.1 ModŁles Formels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.1.2 ReprØsentation graphique . . . . . . . . . . . . . . . . . . . . . . . . 22
3.1.3 RØseaux graphiques vs modŁles mathØmatiques . . . . . . . . . . . . 25
3.2 Forme intermØdiaire de programmes . . . . . . . . . . . . . . . . . . . . . . 27
3.2.1 Graphe d’appel de mØthodes . . . . . . . . . . . . . . . . . . . . . . 27
3.2.2 Graphe d’appel de mØthodes rØparties . . . . . . . . . . . . . . . . . 28
3.3 SØmantique informelle et construction des modŁles . . . . . . . . . . . . . . 32
3.3.1 Construction du rØseau . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.3.2 Comportement d’un futur . . . . . . . . . . . . . . . . . . . . . . . . 36
3.3.3 RŁgles de l’activitØ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.3.4 ModØlisation de la queue de requŒtes . . . . . . . . . . . . . . . . . . 42
3.4 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.4.1 L’objet Philosophe . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.4.2 L’objet Fourchette . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.4.3 Table du D ner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.4.4 VØri cation de propriØtØs d’une application . . . . . . . . . . . . . . 50
3.5 PropriØtØs de la procØdure de construction . . . . . . . . . . . . . . . . . . . 51
3.5.1 Vocabulaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.5.2 PropriØtØs de la pile d’appel . . . . . . . . . . . . . . . . . . . . . . . 52
3.5.3 La procØdure de construction . . . . . . . . . . . . . . . . . . . . . . 53
3.5.4 Le LTS construit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.6 Bilan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4 ModŁles comportementaux paramØtrØs 61
4.1 Abstraction vs instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.2 DonnØes Simples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.3 ModŁles ParamØtrØs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4.3.1 SystŁmes de transitions ØtiquetØes paramØtrØes . . . . . . . . . . . . 64TABLE DES MATI¨RES 9
4.3.2 RØseau de synchronisation paramØtrØ . . . . . . . . . . . . . . . . . . 65
4.4 Structures graphiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
4.4.1 pLTS graphique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
4.4.2 pNet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.4.3 SpØci cations graphiques paramØtrØes vs modŁles paramØtrØs . . . . 68
4.5 Bilan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
5 ModŁles paramØtrØs des applications ProActive 71
5.1 Graphe d’appel de mØthodes paramØtrØ . . . . . . . . . . . . . . . . . . . . 72
5.2 Topologie et Communication . . . . . . . . . . . . . . . . . . . . . . . . . . 75
5.2.1 Structure d’une application . . . . . . . . . . . . . . . . . . . . . . . 75
5.2.2 Messages et Notations . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.2.3 Structure des mØthodes . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.2.4 Objets et Stores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
5.3 Construction des modŁles . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
5.3.1 Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
5.3.2 RØseau global de l’application . . . . . . . . . . . . . . . . . . . . . . 80
5.3.3 RØseau de l’activitØ d’un objet . . . . . . . . . . . . . . . . . . . . . 81
5.3.4 Comportement des Queues . . . . . . . . . . . . . . . . . . . . . . . 82
5.3.5 Proxies de Futurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
5.3.6 Comportement d’une variable dans le Store . . . . . . . . . . . . . . 83
5.3.7 Comportement des mØthodes . . . . . . . . . . . . . . . . . . . . . . 84
5.4 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
5.4.1 Le rØseau de l’application . . . . . . . . . . . . . . . . . . . . . . . . 90
5.4.2 L’objet Philosophe . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
5.4.3 L’objet Fourchette . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5.4.4 VØri cation de propriØtØs . . . . . . . . . . . . . . . . . . . . . . . . 95
5.5 Bilan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
6 Exemples 976.1 Factorielle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
6.2 Nombres de Fibonacci . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
6.3 Arbres binaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
6.4 RØalisation . . . . . . . . . . . . . . . . . . . . . . . .