Composition and Formal Validation in Reactive Adaptive Middleware - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2011

Composition and Formal Validation in Reactive Adaptive Middleware

Résumé

Nowadays, adaptive middleware plays an important role in the design of applications in ubiquitous and ambient computing. Currently most of these systems manage the adaptation at the middleware intermediary layer. Dynamic adaptive middleware are then decomposed into two levels : a first one to simplify the development of distributed systems using devices, a second one to perform dynamic adaptations within the first level. In this report we consider component-based middleware and a corresponding compositional adaptation. Indeed, the composition often involves conflicts between concurrent adaptations. Thus we study how to maintain consistency of the application in spite of changes of critical components and conflicts that may appear when we compose some component assemblies. Relying on formal methods, we provide a well defined representation of component behaviors. In such a setting, model checking techniques are applied to ensure that concurrent access does not violate expected and acceptable behaviors of critical components.
De nos jours, les middlewares adaptatifs et réactifs jouent un role important dans la conception d'applications dans le domaine de l'Informatique ubiquitaire et ambiante. Généralement, ces systèmes réalisent cette adaptation au niveau intermédiaire du middleware. Ainsi, les middlewares adaptatifs sont décomposés en deux parties: une première partie qui permet un développement simplifié des systèmes distribués utilisant des dispositifs, une seconde qui réalise les adaptations dynamiques de la première partie. Dans ce rapport nous considérons des middlewares à base de composants et une adapaptation compositionnelle. Mais souvent lors d'une composition certaines adaptations concurrentes s'avèrent conflictuelles. Pour résoudre ce problème, nous étudions comment préserver la consistence d'une application lors de changements concernant certains composants critiques, avec des conflits qui peuvent apparaitre quand on compose des assemblages de composants. Nous utilisons des méthodes formelles pour modéliser le comportement des composants afin de bénéficier des techniques de vérification par model checking et ainsi prouver que des accès concurrents respectent les comportements acceptables des composants critiques.
Fichier principal
Vignette du fichier
RR-7541.pdf (491.06 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00565860 , version 1 (24-02-2011)
inria-00565860 , version 2 (24-02-2011)

Identifiants

  • HAL Id : inria-00565860 , version 2

Citer

Annie Ressouche, Jean-Yves Tigli, Carillo Oscar. Composition and Formal Validation in Reactive Adaptive Middleware. [Research Report] RR-7541, INRIA. 2011, pp.27. ⟨inria-00565860v2⟩
269 Consultations
159 Téléchargements

Partager

Gmail Facebook X LinkedIn More