p.s.a.: A p-Calculus Static Analyzer¹

Jérôme Feret

Abstract:

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.

• Introduction
• Syntax
  • Input File
  • Operational semantics
  • Unsafe names
• Enforcing a link between agent and the channel names they declare
  • Agent markers
  • Consistency
  • Name markers
• Result
  • Control flow
  • Occurrence counting
• Examples
  • The token-ring
  • An ftp-server
• Conclusion
• References
• Analysis options
• About p-s.a.

This document was translated from L^AT_EX by H^EV^EA and H^AC^HA.