A formal approach to decision support on Mobile Cloud Computing applications

Mobile Cloud Computing (MCC) is an emergent topic growths with the explosion of the mobile applications. In MCC systems, application functionalities are dynamically partitioned between the mobile devices and cloud infrastructures. The main research direction in this field aims at optimizing different metrics, like performance, energy efficiency, reliability and security, in a dynamic environment in which the MCC application is located. Optimization in MCC refers to taking advantages from the offloading process, that consists in moving the computation from the local device to a remote one. The biggest challenge in this aspect is to define a strategy that is able to decide when offloading and which part of the application to move. This technique, in general, improves the efficiency of a system, although sometimes it can lead to a performance degradation. To decide when and what to offload, in this thesis we propose a new general framework supporting the design and the runtime execution of applications on their own MCC scenarios. In particular the framework provides a new specification language, called MobiCa, equipped with a formal semantics that permits to capture all characteristics of a MCC system. Besides the strategy optimization achieved by exploiting the potentiality of the model checker UPPAAL, we propose a set of methods for determining optimal finite/infinite schedules. They are able to manage the resource assignment of components with the aim of improving the system efficiency in terms of battery consumption and time. Furthermore, we propose two optimized scheduling algorithms, developed in Java, based on the exploitation of parallel computation in order to improve the system performance