Well-Typed Services Cannot Go Wrong - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2012

Well-Typed Services Cannot Go Wrong

(1, 2) , (2) , (1, 2) , (1, 2) , (1, 2)
1
2

Abstract

Service-oriented applications are frequently used in highly dynamic contexts: ser- vice compositions may change dynamically, in particular, because new services are discovered at runtime. Moreover, subtyping has recently been identified as a strong requirement for service dis- covery. Correctness guarantees over service compositions, provided in particular by type systems, are highly desirable in this context. However, while service oriented applications can be built using various technologies and protocols, none of them provides decent support ensuring that well-typed services cannot go wrong. An emitted message, for instance, may be dangling and remain as a ghost message in the network if there is no agent to receive it. In this article, we introduce a formal model for service compositions and define a type system with subtyping that ensures type soundness by combining static and dynamic checks. We also demonstrate how to preserve type soundness in presence of malicious agents and insecure communication channels.
Les applications orientées services (SOA) sont hautement dynamiques car la con- naissance et la topologie des services évoluent au cours du temps. La découverte dynamique des services est une facilité importante des SOA, sa flexibilité et sa puissance d'utilisation a été récemment accrue par l'introduction d'une notion de sous-typage. Dans un tel contexte des garanties sur la composition des services est un besoin crucial pour le passage à l'échelle. Les systèmes de types sont connus dans le contexte de la programmation pour permettre certaines garanties minimales. Toutefois, les technologies actuelles des services sont très hétérogènes, et aucune proposition n'a vraiment été faite pour un système de type décent. Un tel système de type doit supporter des canaux de première classe, une relation de sous-typage et assurer qu'un message émis ne restera pas un fantôme dans le réseau de communication. Un message fantôme est un message émis qui ne vérifierait pas le contrat minimal pour être reçu par un agent et se trouve donc à demeurer éternellement dans le réseau. Dans cet article nous introduisons un modèle formel pour des services indépendant de leur orchestration et nous définissons un système de type sémantique. Ce modèle avec son système de type assure une propriété de correction : tous les messages émis par un agent pourront être reçus par l'agent destinataire. Nous prouvons également que cette propriété est satisfaite dans des contextes où certains agents ne sont pas fiables et en présence de canaux de communications non sûrs.
Fichier principal
Vignette du fichier
main.pdf (977.98 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00700570 , version 1 (23-05-2012)
hal-00700570 , version 2 (02-07-2012)

Identifiers

  • HAL Id : hal-00700570 , version 2

Cite

Diana Allam, Rémi Douence, Hervé Grall, Jean-Claude Royer, Mario Südholt. Well-Typed Services Cannot Go Wrong. [Research Report] RR-7899, INRIA. 2012. ⟨hal-00700570v2⟩
284 View
273 Download

Share

Gmail Facebook Twitter LinkedIn More