A Formal Model of a Cloud Service Architecture in terms of ambient ASM

This document presents a formal model of a cloud service system in terms of Ambient Abstract State Machine in two abstraction layer: while the spatial locations, mobility and some security considerations (accessibility) are described by a hierarchy of some ambient constructs; the algorithmic functionalities are defined by abstract state machine agents (which reside on various locations in the ambient hierarchy). The proposed model applies a novel approach for client-cloud interaction by which service owners, who may be different from the cloud provider, are able to fully control the usages of their services in the case of each subscription, respectively.