Modeling and formal analysis of a client-server application for cloud services

In the context of Cloud computing, a service can be invoked by distinct devices having different HW/SW characteristics; therefore, the content must be adapted to each device profile. A solution consists in having a middleware server that receives requests from the clients, forwards them to the cloud, and adapts the answers coming from the cloud on the base of device profiles. This paper proposes a formalization of this framework using Abstract State Machines (ASMs). The modeling process is based on the ASMs refinement method, and has been guided and supported by several validation and verification activities to guarantee consistency, correctness, and reliability properties.