| Titre : | Une Approche formelle pour les applications WEB 2.0 |
| Auteurs : | Mohammed Charaf Eddine Meftah, Auteur ; Okba Kazar, Directeur de thèse |
| Type de document : | Thése doctorat |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2016 |
| ISBN/ISSN/EAN : | TINF/93 |
| Format : | 1 vol. (147 p.) / ill. / 29 cm |
| Langues: | Français |
| Résumé : |
Ce travail propose une approche formelle pour le développement des applications Web 2.0 sûres.Cette approche consiste en la génération d'une implémentation de l’application à partir de spécifications formelles. On décrit préalablement l'application à l'aide de notations (CTT), puis un processus automatique est appliqué afin de les traduire en spécifications formelles B. En utilisant le processus de raffinement B, un ensemble de règles de raffinement, opérant sur les opérations, est appliqué sur les spécifications ainsi obtenues. Ces règles considèrent l’aspect dynamique (opérations) de l’application Web étudiée ; ces phases de raffinement ont pour but de rendre les spécifications finales proches des langages d'implémentations cibles choisi (WS-BPEL, JAVA), de telle sorte que la dernière phase de codage devienne intuitive et naturelle. De manière générale, le processus de raffinement est une tâche manuelle, relativement coûteuse, en particulier en phase de preuve. Grâce au caractère générique de ces règles de raffinement, un outil de raffinement assisté peut être réalisé,permettant ainsi la réduction du coût du processus de raffinement. |
| Sommaire : |
Chapitres 1 : Introduction Générale............................10 I.1 Le contexte......................................10 I .2 Les problématiques et les motivations................................................13 I .3 L’objectif....................................................................14 I.4 La démarche....................................15 I.5 Contributions............. ……..................15 I.6 L’organisation de la thèse ...............16 Chapitres 2 : Etat de l’art de Web 2+............................................................17 II.1. Introduction ................................18 II.2. Définitions ............................................19 II.3. L’aspect Social de Web 2............................22 II.4. Les Architectures Orientées Service ......23 II.4.1 Les services ............................23 II.4.2 Le modèle de référence OASIS ..................................24 II.4.3 Les architectures orientées service Web ........................25 II.4.3.1 Les services web...................................25 II.4.3.2 Les différentes couches de l’architecture orientés service Web ...................28 II.4.3.2. 1. La couche Transport.............................................29 II.4.3.2. 2. La couche communication (messages) ....................30 SOAP.............................................30 II.4.3.2. 3. La couche description ...................32 UDDI.............................34 Le Web sémantique.............................................................34 II.4.3.2. 4 La couche qualité de service ....................................36 II.4.3.2. 5. La sécurité ..................................................36 II.4.3.2. 6. La couche processus ..................................37 La chorégraphie...............................................................37 WSCI..............................................................38 WS-CDL .................................................................................38 L’orchestration .................................................. 39 XLANG.......................................……….......................40 WSFL................................….........................................40 BPML.................................................................40 Le langage BPEL .......................................................................41 II.5. Les bases technologiques du Web .............................44 II.5.1 Représentation de technique de l’approche AJAX ......................................................44 II.5.2 Le principe AJAX...................................................................45 II.5.3 Les frameworks Java WEB....................................................................47 II.5.4 Les caractéristiques de java .......................................................48 II.5.5 Le développement des interfaces graphiques..............................................................51 II.5.5.1 Les éléments d'interfaces graphiques de l'AWT .......................................................52 II.5.5.2 L'interception des actions de l'utilisateur avec Java ..................................................54 II.5.6 Principes de la programmation par événement...........................................................55 II.5.6.1 Modèle de délégation de l'événement en Java........................................................55 II.5.6.2 Notion d’état d’un objet.........................................56 II.5.6.3 Notion de comportement d’un objet.................................................56 1.5.6.4 Les opérations.......................................................56 II.5.6.5 Rôle et responsabilités................................................57 II.5.6.6 Les objets en tant que machines............................................58 II.5.7 Programme Java-Swing..................................................58 II.5.7.1 Structure...............................................................58 II.5.7.2 Contrôle de flux................................................58 II.6 Conclusion ...................................................................60 Chapitre 3 : (Les travaux Liés) : ..............................................62 III.1 Introduction............................................................63 III.2 Les systèmes de transitions LTSA-WS ..............................................64 III. 3 Les réseaux de Pétri ..................................................66 III.4 Les algèbres de processus ..................................67 III.5 ASDL.............................................................68 III.6 LOTOS/CADP……………..……………..…………..69 III.7 Le π –calcul .........................................................................72 III. 8 Les théories temporelles................................................73 III. 9 Les logiques temporelles................................................74 III. 11 Les logiques temporelles arborescentes basées sur actions……..…..………………...76 III. 12 La logique ACTL........................................................76 III. 13 L’approche Diapason .........................................................................78 III. 14 Approche dirigée par les modèles (MDA-UML-S) ...................................................80 III. 15 Autres formalismes ..............................................................81 III. 16 Synthèse et Conclusion.............................................................82 Chapitre 4 : (L’approche proposée ) ………….………………….…….…..86 IV.1 Introduction………………………………………………………….………………..….87 IV.2 L’approche proposée…………………………………………..………………………... 88 IV.2.1 Les techniques utilisées………………………………….………………..…………….91 IV.2.1.1 CTT (Concur Task Tree) …………………………………………..…….…………91 IV.2.1.2 La méthode formelle B …………………………………………..………...………92 IV.2.2 Meta Model et Liens structurels entre spécifications B, Service Web et diagrammes de classes (Java) ……………………94 IV.2.3 L’Architecture générale de l’approche proposée ………………….…………………..97 IV.2.4 Modèle pour la spécification ………………………………………….……………….99 IV.2.5 Modèle pour la vérification et la validation …………………………………………100 IV.2.6 Modélisation des propriétés statiques et dynamiques………………………………..102 IV.2.7 Le raffinement……………………………………………………………………….103 IV.2.7.1 Les types de raffinement ……………………………………………..……..…..…103 IV.2.7.2 La dépendance des messages …………………………………..…..……………..104 IV.2.7.3 Niveaux des raffinements proposées pour les applications Web2+…………………...…...104 IV.2.8 La décomposition de complexités en B pour une application Web 2+………...….109 IV.2.9 Développement pratique pour la génération automatique de code……………….….111 IV.2.9.1 Structure générale …………………………………………………………………………111 IV.2.9.2 Les Règles de traduction ………………………………………………………….112 IV.2.9 .2.1 Les règles de codage descendant (B-BPEL4SW)……………………………...112 IV.2.9 .2.2 La traduction ascendante (BPEL4SW-B) ………………..………………………..…112 IV.2.9 .2.3 Les règles de codage descendante (B-JAVA) …………………………….…114 IV.2.9 .2.4 La traduction ascendante (JAVA-B) …………………………………………..114 IV.3 Conclusion ……………………………………………………………………….…………….118 Chapitre 5 : (Etude de cas ) ………………………………………………………………………119 V.1 Introduction………………………………………………………………………….……….…120 V.2 Préparation de l'environnement de développement……………….……………………………122 V.3 Composition des services de l’application (Processus BPEL4SW)…….……………………...122 V.3.1 Définir les liens partenaires des services Web concernés (importation des fichiers WSDL externes) ……………………122 V.3.1.2 Définir la logique du processus (des notations CTT)…………………………..............…124 V.3.1.3 La traduction en spécifications formelles B……………………………..…………….….125 V.3.1. 4 La génération automatique de code source (BPEL4SW)………………………..………126 V.4 Le comportement de l'interface de l’application agence de voyage……………………………129 V.4.1 Spécifications formelles B de l’interface de l’application……………………………….…..130 V.4.2. La génération automatique de code source (JAVA)…………………………………..……135 V.5 Outils B: Click'n prouve et B4free……………………………….…………………………...137 V.1 Comparaison …………………………………………………………………………..……..139 V.2 Conclusions générales et perspectives ;;………………………………...………………140 Bibliographies………………………………….………………………………...………………142 |
| En ligne : | http://thesis.univ-biskra.dz/id/eprint/2501 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/93 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
