Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Jérôme Feret Connect in order to contact the contributor
Submitted on : Wednesday, October 20, 2010 - 3:44:47 PM
Last modification on : Thursday, March 17, 2022 - 10:08:35 AM

Links full text




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⟩



Record views