Skip to Main content Skip to Navigation
Reports

Preuve de propriétés de comportement deprogrammes ProActive

Rabea Boulifa 1 Eric Madelaine
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
Résumé : Nous étudions les méthodes de preuve des propriétés comportementales d'applications Java distribuées dans lesquelles les objets sur des sites différents coopèrent par appels distants de méthodes. La bibliothèque ProActive fournit un moyen simple et efficace pour mettre en oeuvre cette coopération par définition de primitives qui facilitent la programmation distribuée. Nous présentons une méthode pour définir des modèles comportementaux, compositionne- ls, pour ces applications distribuées, en nous restreignant au cas sans création dynamique d'objets actifs. Nous montrons comment prouver que certaines approximations finies du modèle d'un objet actif représentent fidèlement son comportement. L'analyse des propriétés de l'application (recherche d'inter-blocage, preuves de propriétés de sûreté) peut alors être conduite, sur ces modèles finis compositionnels, en utilisant des outils de vérification automatiques basés sur une sémantique comportementale par bisimulation. Ces analyses compositionnelles ne nécessitant pas de construire l'espace d'états global, souffrent moins du problème d'explosion de l'espace d'état que la plupart des approches du model-checking.
Document type :
Reports
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072128
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:51:23 PM
Last modification on : Friday, January 8, 2021 - 11:14:19 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:54:33 PM

Identifiers

  • HAL Id : inria-00072128, version 1

Collections

Citation

Rabea Boulifa, Eric Madelaine. Preuve de propriétés de comportement deprogrammes ProActive. RR-4460, INRIA. 2002. ⟨inria-00072128⟩

Share

Metrics

Record views

260

Files downloads

239