Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL

Ludovic Henrio 1 Muhammad Uzair Khan 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Components provide an easy to use programming paradigm allowing for better re-usability of application code. In the context of distributed programming, autonomous hierarchical components provide a simple model for creating efficient applications. This paper presents a model for distributed components communicating asynchronously using futures – placeholders for results. Our components communicate via asynchronous requests and replies where the requests are enqueued at the target component, and the invoker receives a future. Then, future references can be dispersed among components. When the result is available for a future, it needs to be transmitted to all interested components, as determined by a future update strategy. We present formal semantics of our component model incorporating formalisation of one such future update strategy. Our model has been mechanically formalised in Isabelle/HOL, together with the proof of properties. This approach validates the actual implementation of the future update strategy itself.
Type de document :
Communication dans un congrès
7th International Workshop on Formal Engineering approaches to Software Components and Architectures, Mar 2010, Paphos, Cyprus. pp.1-20, 2010
Liste complète des métadonnées


https://hal.inria.fr/inria-00462325
Contributeur : Muhammad Uzair Khan <>
Soumis le : vendredi 28 mai 2010 - 16:02:14
Dernière modification le : vendredi 28 mai 2010 - 17:07:18
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 14:16:07

Fichier

FutureUpdateGCM.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00462325, version 1

Collections

Citation

Ludovic Henrio, Muhammad Uzair Khan. Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL. 7th International Workshop on Formal Engineering approaches to Software Components and Architectures, Mar 2010, Paphos, Cyprus. pp.1-20, 2010. <inria-00462325>

Partager

Métriques

Consultations de
la notice

274

Téléchargements du document

126