Formal analysis of seamless application execution in mobile cloud computing

Mobile cloud computing augments the resource-constrained mobile devices to run rich mobile applications by leveraging the cloud resources and services. Compute-intensive mobile apps require significant communication resources for migrating the code from mobile devices to the cloud. For such apps, distributed application execution frameworks (DAEF) have been proposed in the literature. These frameworks either migrate the mobile app code during runtime or keep the app synchronized with another remotely executed app on the cloud. Frameworks also support mobile app live migration to cater for compute node mobility. One key research question arises is how successful are these DAEFs in achieving the seamless application execution under various network conditions? The answer to this question entails formal analysis of the DAEFs to determine the realistic bounds on propagation delay, bandwidth and application interaction with mobile device for various types and sizes of apps. In this research, we apply formal analysis techniques to define the execution time of the app and the time required for code migration. We also define three conditions for seamless application execution. Given realistic values for processor speed, application executable size, possible number of executed instructions, network propagation delay and transmission delay, we show what components of the mobile app need to be migrated during execution to the cloud. Finally, we compute realistic bounds for the app size (that can be executed seamlessly) based on important features which include cloud and device resources, bandwidth and latency profile.