Abstract Interpretation of Mobile Systems
Résumé
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.