p.s.a.: A p-Calculus Static Analyzer1
p-s.a. is an academic tool for statically inferring a sound description of the potential behaviour of a mobile system interacting with an unknown context.
It uses Abstract Interpretation to infer two kinds of properties: the control flow and the occurrence number of agent instances.
Control flow analysis captures all the potential interactions between agents, it is precise enough to distinguish between recursive instances of the same agent.
Occurrence counting analysis enable us to detect mutual exclusion between agents and non-exhaustion of resources.
This document was translated from LATEX by
HEVEA and HACHA.