Decision Support for Mobile Cloud Computing Applications via Model Checking

Deciding whether to off load some computation is a crucial issue in Mobile Cloud Computing systems. This paper proposes a new methodology, whose goal is to provide runtime support for off loading decisions, based on a formal framework. By means of a domain specific language (MobiCa), a developer can define both system and application structure. Using the diagnostic trace generated at runtime by the well-known model checker UPPAAL, driven by some query verified on the timed automata model associated with the MobiCa specification, the framework decides which application fragments should be remotely executed. The proposed approach is exemplified on a navigator case study, probably one of the most used applications on mobile devices.