Formal Modeling of a Client-Cloud Interaction Middleware with respect to Adaptivity

Cloud computing is no longer a new paradigm, but it became very popular in the recent years and its adoption is still growing. One circumstance of this increase is the merging of cloud computing with various domains (e.g.: Mobile Cloud Computing (MCC)), visions (e.g.: Internet of Things (IoT)) and popular terms (e.g.: Big Data). MCC emerged with the aim of overcoming the limitations of mobile devices: restricted storage, scarce computation capacity, and tight energy. However, the join of cloud computing with mobile computing leads to other challenges, like network variability and mobility. To expand the applicability of cloud services, a cloud system architecture should guarantee that clients with various end-devices (desktop computers, laptops, tablets, smartphones, etc.), that are running different operating systems, owning distinct hardware characteristics (e.g.: processor speed, display size, resolution, etc.) receive the highest possible Quality of Service (QoS). Therefore automatic, on-the-fly adaptivity of cloud services to different end-devices and network environment is required, in particular with respect to needs arising from mobile clients. The main contribution of this thesis is the formal specification and analysis of an adaptivity component, as part of a middleware application, that is responsible for adapting the cloud service content to different device profiles and changing network conditions. The main objectives of this work are: to determine the appropriate approach for layout and content adaptation regarding device and network characteristics, provide a formal design of the system, and validate and verify the high-level specifications.