Abstract
Energy consumption is one of the primary non-functional properties to be addressed early in software system development. Model-based analysis methods are introduced in order to supplement the current practice of runtime profiler techniques. In the present paper, the energy consumption analysis is classified as a duration bounded cost constraint problem. Specifically, behavioral contracts based on Power Consumption Automata and properties written in terms of weighted linear temporal logic with freeze quantifiers are proposed. In addition, the problem is solved by model-checking of such logic formulas with respect to the automaton.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Android, http://developer.android.com
Alur, R., Courcoubetis, C., Henzinger, T.A.: Computing Accumulated Delays in Real-Time System. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 181–193. Springer, Heidelberg (1993)
Alur, R., Henzinger, T.A.: A Really Temporal Logic. J. Accoc. Comp. Machin. 41(1), 181–204 (1994)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theor. Comp. Sci. 138, 3–24 (1995)
Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: Minimum-Cost Reachability for Priced Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)
Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed Automata with Observers under Energy Constraints. In: Proc. HSCC 2010 (2010)
Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Li, G., Bøgsted Poulsen, D., Stainer, A.: Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 168–182. Springer, Heidelberg (2012)
Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Processing Letters 40, 269–276 (1991)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: 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)
Demri, S., Lazić, R., Nowak, D.: On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. Information and Computation 205(1), 2–24 (2007)
Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model Checking Duration Calculus: a practical approach. Formal Aspects of Computing 20, 481–505 (2008)
Nakajima, S.: Model-based Power Consumption Analysis of Smartphone Applications. In: Proc. ACES-MB 2013 (2013)
Nakajima, S.: Everlasting Challenges with the OBJ Language Family. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Futatsugi Festschrift. LNCS, vol. 8373, pp. 478–493. Springer, Heidelberg (2014)
Nakajima, S.: Platform-Dependence in Model-based Energy Consumption Analysis of Smartphone Applications. NII Technical Report (2014)
Ölveczky, P.C., Meseguer, J.: Semantics and Pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)
Ölveczky, P.C., Meseguer, J.: Abstraction and Completeness for Real-Time Maude. ENTCS 176(4), 5–27 (2007)
Ouaknine, J., Worrell, J.: Some Recent Results in Metric Temporal Logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008)
Pathak, A., Hu, Y.C., Zhang, M.: Bootstrapping Energy Debugging on Smartphones: A First Look at Energy Bugs in Mobile Devices. In: Proc. Hotnets 2011 (2011)
Pathak, A., Hu, Y.C., Zhang, M.: Where is the energy spent inside my app?: Fine Grained Energy Accoutning on Smartphones with Eprof. In: Proc. EuroSys 2012 (2012)
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. Statistical Probablistic Model Checking. J. STTT 8(3), 216–228 (2006)
Zhang, L., Gordon, M.S., Dick, R.P., Mao, Z.M., Dinda, P., Yang, L.: ADEL: An Automatic Detector of Engery Leaks for Smartphone Applications. In: Proc. CODES+ISSS 2012 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Nakajima, S. (2015). Model Checking of Energy Consumption Behavior. In: Cardin, MA., Krob, D., Lui, P., Tan, Y., Wood, K. (eds) Complex Systems Design & Management Asia. Springer, Cham. https://doi.org/10.1007/978-3-319-12544-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-12544-2_1
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12543-5
Online ISBN: 978-3-319-12544-2
eBook Packages: EngineeringEngineering (R0)