Parameterized Models for Distributed Java Objects

Tomás Barros 1 Rabea Boulifa 1 Eric Madelaine 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models capturing the behavioural semantics of ProActive objects. Our models are symbolic networks of labelled transition systems, whose labels represent (abstractions of) remote method calls. In contrast to the usual finite models, they encode naturally and finitely a large class of distributed object-oriented applications. Their finite instantiations can be used in classical model-checkers and equivalence-checkers for checking temporal logic properties in a compositional manner. We are building a software tool set for the analysis of ProActive applications using these methods.
Type de document :
Communication dans un congrès
Forte'04 conference, Sep 2004, Madrid, Spinger Verlag, LNCS 3235, 2004
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
Contributeur : Eric Madelaine <>
Soumis le : vendredi 21 juillet 2006 - 15:34:06
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:21:20



  • HAL Id : inria-00087222, version 1



Tomás Barros, Rabea Boulifa, Eric Madelaine. Parameterized Models for Distributed Java Objects. Forte'04 conference, Sep 2004, Madrid, Spinger Verlag, LNCS 3235, 2004. 〈inria-00087222〉



Consultations de la notice


Téléchargements de fichiers