Formal Modeling of Mobile Computing Systems Based on Ambient Abstract State Machines

In this paper, we present a high-level definition of a formal method in terms of ambient abstract state machine rules which makes it possible to describe formal models of mobile computing systems and complex service oriented architectures in two abstraction layers. This means that while the algorithms and local interactions of executable components (agents) are specified in terms of abstract state machines; the long-term interactions as well as movements of various components via various administrative domains are given in terms of ambient calculus in our approach.