Abstract interpretation of mobile systems

AbstractWe propose an Abstract Interpretation-based context-free analysis for mobile systems written in the π-calculus. Our analysis automatically captures a sound—but not complete—description of the potential behavior 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 a 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 instances of agents. Our abstraction is relational; this makes us able to detect both quickly and precisely mutual exclusion and non-exhaustion of resources