Abstract Interpretation of Mobile Systems

Abstract : We propose an Abstract Interpretation-based context-free analysis for mobile systems written in the pi-calculus. Our analysis automatically captures a sound -- but not complete -- description of the potential behaviour of a mobile system interacting with an unknown context. It focuses on both the control flow and the occurrence number of agents during computation sequences. Control flow analysis detects all the possible interactions between the agents of the system, but also the potential interactions with the context. In order to deal with dynamic creation of both names and agents which is an inherent feature of mobility, our analysis distinguishes between recursive instances of the same agent. This way, we are able to prove the integrity of an ftp-server used by an unbounded number of clients. Occurrence counting analysis just consists in abstracting the occurrence number of syntactic agents. Our abstraction is relational; this makes us able to detect both quickly and precisely mutual exclusion and non-exhaustion of resources.
Type de document :
Article dans une revue
Journal of Logic and Algebraic Programming, Elsevier, 2004, special issue on the pi-calcucus, 63 (1), pp.59--130. 〈10.1016/j.jlap.2004.01.005〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00527910
Contributeur : Jérôme Feret <>
Soumis le : mercredi 20 octobre 2010 - 15:44:47
Dernière modification le : mardi 24 avril 2018 - 17:20:12

Lien texte intégral

Identifiants

Collections

Citation

Jérôme Feret. Abstract Interpretation of Mobile Systems. Journal of Logic and Algebraic Programming, Elsevier, 2004, special issue on the pi-calcucus, 63 (1), pp.59--130. 〈10.1016/j.jlap.2004.01.005〉. 〈inria-00527910〉

Partager

Métriques

Consultations de la notice

225