Abstract
Computation offloading is a key concept in Mobile Cloud Computing: it concerns the capability of moving application components from a mobile device to the cloud. 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, we propose the use of a method for determining an optimal infinite scheduler, which is able to manage the resource assignment of components with the aim of improving the system efficiency in terms of battery consumption and time. In particular, in this paper we define a cost/reward horizon method for Mobile Cloud Computing systems specified in the language MobiCa. By means of the model checker UPPAAL, we synthesize an optimal infinite scheduler for a given system specification. We assess our approach through a case study, which highlights the importance of a scheduler for reducing energy consumption and improving system performance.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Fernando, N., Loke, S.W., Rahayu, W.: Mobile cloud computing: a survey. Future Gener. Comput. Syst. 29(1), 84–106 (2013)
Flinn, J.: Cyber foraging: bridging mobile and cloud computing. Synth. Lect. Mob. Pervasive Comput. 7(2), 1–103 (2012)
Kumar, K., Lu, Y.H.: Cloud computing for mobile users: can offloading computation save energy? Computer 43(4), 51–56 (2010)
Aceto, L., Morichetta, A., Tiezzi, F.: Decision support for mobile cloud computingapplications via model checking. In: MobileCloud, vol. 1, pp. 296–302. IEEE (2015)
Bulychev et al.: UPPAAL-SMC: statistical model checking for priced timed automata. arXiv preprint arXiv:1207.1272 (2012)
Gruian, F., Kuchcinski, K.: Low-energy directed architecture selection and task scheduling for system-level design. In: EUROMICRO, pp. 1296–1302. IEEE (1999)
MobiCa, U.: Model. http://www.amorichetta.eu/MobiCa/m_u_model.zip
Cuervo, et al.: MAUI: making smartphones last longer with code offload. In: MobiSys, pp. 49–62. ACM (2010)
Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Meth. Syst. Des. 32(1), 3–23 (2008)
Rasmussen, J.I., Larsen, K.G., Subramani, K.: On using priced timed automata to achieve optimal scheduling. Formal Meth. Syst. Des. 29(1), 97–114 (2006)
Larsen, K.G., Mikučionis, M., van Vliet, J., Wang, Z., David, A., Legay, A., Poulsen, D.B.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011)
Rudenko, A., Reiher, P., Popek, G.J., Kuenning, G.H.: The remote processing framework for portable computer power saving. In: SAC, pp. 365–372. ACM (1999)
Flinn, J., Park, S., Satyanarayanan, M.: Balancing performance, energy, and quality in pervasive computing. In: Distributed Computing Systems, pp. 217–226 (2002)
Balan, R.K., Satyanarayanan, M., Park, S.Y., Okoshi, T.: Tactics-based remote execution for mobile computing. In: MobiSys, pp. 273–286. ACM (2003)
Ra, M. et al.: Odessa: enabling interactive perception applications on mobile devices. In: MobiSys, pp. 43–56. ACM (2011)
Acknowledgements
Luca Aceto has been supported by the projects ‘Nominal Structural Operational Semantics’ (nr. 141558-051) of the Icelandic Research Fund and ‘Formal Methods for the Development and Evaluation of Sustainable Systems’, grant under the Programme NILS Science and Sustainability, Priority Sectors Programme of the EEA Grants Framework. Kim G. Larsen is supported by the SENSATION FET project, the Sino-Danish Basic Research Center IDEA4CPS, the Innovation Fund Center DiCyPS and the ERC Advanced Grant LASSO. Andrea Morichetta and Francesco Tiezzi have been supported by the EU projects ASCENS (257414) and QUANTICOL (600708) and by the MIUR PRIN project CINA (2010LHT4KM).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Aceto, L., Larsen, K.G., Morichetta, A., Tiezzi, F. (2016). A Cost/Reward Method for Optimal Infinite Scheduling in Mobile Cloud Computing. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-28934-2_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-28933-5
Online ISBN: 978-3-319-28934-2
eBook Packages: Computer ScienceComputer Science (R0)