Amb-s.a.: A Static Analyzer for Mobile Ambients¹
Version 1.01

Jérôme Feret

Abstract:

Amb-s.a. is an academic tool for statically inferring a sound description of the potential behaviour of a mobile system described in the Ambient-calculus. It uses Abstract Interpretation to infer both the control flow and occurrence number properties: Control flow analysis captures all the potential interactions between agents, it is precise enough to distinguish between recursive instances of the same agent. Occurrence number analysis captures both the number of agents that may be contained inside an ambient, and the number of agents that may occurs inside the whole system.

• Introduction
• Syntax
  • Input File
  • Operational semantics
• Enforcing a link between agent and the channel names they declare
  • Agent markers
  • Consistency
  • Name markers
• Result
  • Communication analysis
  • Migration analysis
  • Content analysis
  • Global occurrence analysis
• Examples
  • An ftp-server
• Conclusion
• References
• Analysis options
• About Amb-s.a.

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