| Titre : | Spécification et vérification de système a' base de SOA en utilisant l’algèbre de processus |
| Auteurs : | souad Ababsa, Auteur ; Amira Mohammedi, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2019 |
| Format : | 1 vol. (54 p.) / ill. / 29 cm |
| Langues: | Français |
| Résumé : |
De nos jours, les services web sont devenus tr?es utilisés notamment par les en-treprises pour rendre accessibles leurs métiers et leurs données via le web. La composition des services web est un sujet qui suscite l'intér^et des chercheurs.Elle oére la possibilité de traiter des problémes complexes m^eme avec des services simples existants tout en coopérant entre eux. Toutefois, cette t^ache reste trés complexe et nécessite, pour assurer sa ?abilité, des techniques formelles. L'objectif principal de notre travail est de spéci?er formellement une composition de services web, illustrée dans le cas d'une agence de voyage.Il existe plusieurs outils formels de spéci?cation, dont l'algébre de processus qui oére un moyen éa la fois puissant et relativement succinct pour sp?eci?er des systémes complexes. Nous avons choisi le langage LOTOS qui permet,outre la spéci?cation des processus, la représentation des données. Nous avons utilisé l'outil CADP pour la véri?cation de notre spéci?cation. |
| Sommaire : |
Introduction xi I Etat de l’art 1 1 Architecture Orientée Service et Services Web 2 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.1 Principes des SOAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Avantages des SOAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Inconvénients des SOAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Services Web . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4.1 Objectifs des services Web . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4.2 Caractéristiques des services Web . . . . . . . . . . . . . . . . . . . . 7 1.4.3 Composition des services Web . . . . . . . . . . . . . . . . . . . . . . 8 1.4.3.1 Orchestration . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4.3.1.1 Business Process Execution Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4.3.1.2 Avantages de l’orchestration . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4.3.2 Chorégraphie . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2 Approches formelles 12 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1 Définition des approches formelle . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2 Approches basées sur la logique . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.1 Méthode B . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.1.1 Avantages de méthode B . . . . . . . . . . . . . . . . . . . . 13 2.2.1.2 Inconvénients de la méthode B . . . . . . . . . . . . . . . . 13 2.3 Approches par modèles à états . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3.1 SDL (Specification and Description Langage) . . . . . . . . . . . . . 14 2.3.1.1 Avantage de SDL . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3.2 RDP (Réseau de Petri) . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3.2.1 Avantage de RDP . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.2.2 Inconvénient de RDP . . . . . . . . . . . . . . . . . . . . . . 15 2.4 Approches algébriques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.4.1 CCS (Calculus Communicating Systems) . . . . . . . . . . . . . . . . 15 2.4.1.1 Avantage de CCS . . . . . . . . . . . . . . . . . . . . . . . . 16 2.4.1.2 Inconvénient de CCS . . . . . . . . . . . . . . . . . . . . . . 16 2.4.2 LOTOS (Language Of Temporal Ordering Specification) . . . . . . . 16 2.4.2.1 Avantage de LOTOS . . . . . . . . . . . . . . . . . . . . . . 17 2.5 Travaux connexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.6 Algèbre de Processus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.7 Comparaison entre CCS et LOTOS . . . . . . . . . . . . . . . . . . . . . . . 20 2.8 Caractéristiques principales d’algèbre de processus . . . . . . . . . . . . . . . 20 2.9 Langage Of Temporal Ordering Specification . . . . . . . . . . . . . . . . . . 21 2.9.1 Syntaxe formelle de LOTOS . . . . . . . . . . . . . . . . . . . . . . . 22 2.9.1.1 Basic-LOTOS . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.9.1.2 Full-LOTOS . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.9.1.2.1 Abstract Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.9.2 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.10 Outil de spécification et vérification pour LOTOS . . . . . . . . . . . . . . . 29 2.10.1 Construction and Analysis of Distributed Processes . . . . . . . . . . 29 2.10.2 Principe d’usage de CADP . . . . . . . . . . . . . . . . . . . . . . . . 29 2.10.3 Propriétés de vérification . . . . . . . . . . . . . . . . . . . . . . . . . 31 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 II Spécification et Vérification 33 3 Spécification formelle 34 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.1 Analyse du système . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.1.1 Architecture du système de l’agence du voyage . . . . . . . . . . . . . 35 3.1.2 Diagrammes de séquence . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.1.3 Spécification de l’application avec LOTOS . . . . . . . . . . . . . . . 38 3.1.4 Implémentation des processus avec lotos . . . . . . . . . . . . . . . . 40 3.1.4.1 Processus initial . . . . . . . . . . . . . . . . . . . . . . . . 40 3.1.4.2 Processus client . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.1.4.3 Processus sequence . . . . . . . . . . . . . . . . . . . . . . . 40 3.1.4.4 Processus agence du voyage . . . . . . . . . . . . . . . . . . 41 3.1.4.5 Rôle du processus parallelsplit . . . . . . . . . . . . . . . . . 41 3.1.4.6 Processus de réservation de vol . . . . . . . . . . . . . . . . 42 3.1.4.7 Processus sequence1 de reservation-ok . . . . . . . . . . . . 42 3.1.4.8 Processus sequence2 de reservation-not . . . . . . . . . . . . 42 3.1.4.9 Processus sequence3 de payement-ok . . . . . . . . . . . . . 42 3.1.4.10 Processus sequence4 de payement-not . . . . . . . . . . . . . 43 3.1.4.11 Processus de réservation hôtel . . . . . . . . . . . . . . . . . 43 3.1.4.12 Processus de réservation voiture . . . . . . . . . . . . . . . . 43 3.1.4.13 Processus de la banque . . . . . . . . . . . . . . . . . . . . . 44 3.1.4.14 Processus final . . . . . . . . . . . . . . . . . . . . . . . . . 44 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 4 Vérification formelle 46 4.1 Installation de CADP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4.2 Exécution de la spécification . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.2.1 Arbre de spécification . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4.2.2 Labelled Transition System . . . . . . . . . . . . . . . . . . . . . . . 51 4.3 Vérification formelle avec CADP . . . . . . . . . . . . . . . . . . . . . . . . . 52 4.3.1 Propreté de safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.3.2 Propreté de atteignabilité . . . . . . . . . . . . . . . . . . . . . . . . 53 Conclusion x Bibliography xvii |
| Type de document : | Mémoire master |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/481 | Mémoire master | bibliothèque sciences exactes | Consultable |
