Abstract
Energy consumption is one of the primary non-functional concerns, especially for application programs running on systems that have limited battery capacity. A model-based analysis of energy consumption is introduced at early stages of development. As rigorous formal models of this, the power consumption automaton and a variant of linear temporal logic are proposed. Detecting unexpected energy consumption is then reduced to a model checking problem, which is unfortunately undecidable in general. This paper introduces some restrictions to the logic formulas representing energy consumption properties so that an automatic analysis is possible with Real-Time Maude.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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. Assoc. 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., Pettersson, P., Romjin, J., Vaandrager, F.: Minimum-Cost Reachability for Priced Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)
Brekling, A., Hansen, M.R., Madsen, J.: MoVES – A Framework for Modeling and Verifying Embedded Systems. In: Proc. ICM 2009, pp. 149–152 (2009)
Cassez, F., Larsen, K.G.: The Impressive Power of Stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000)
Clavel, M., Duran, F., Eker, S., Lincoln, P., Marti-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Demri, S., Lazic, R., Nowak, D.: On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. Information and Computation 205(1), 2–24 (2007)
Lepri, D., Olveczky, P.C., Abraham, E.: Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specification. In: Proc. RTRTS 2010, pp. 117–136 (2010)
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 2014. LNCS, vol. 8373, pp. 478–493. Springer, Heidelberg (2014)
Nakajima, S.: Model Checking of Energy Consumption Behavior. In: Proc. 1st CSDM Asia, pp. 3–14 (2014)
Nakajima, S., Toyoshima, M.: Behavioral Contracts for Energy Consumption. Ada User Journal 35(4), 266–271 (2014)
Olveczky, P.C., Meseguer, J.: Semantics and Pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)
Olveczky, 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., Bahl, P., Wang, Y.-M.: Fine-Grained Power Modeling for Smartphones Using System Call Tracing. In: Proc. EuroSys 2011 (2011)
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 Accounting on Smartphones with Eprof. In: Proc. EuroSys 2012 (2012)
Zhang, L., Gordon, M.S., Dick, R.P., Mao, Z.M., Dinda, P., Yang, L.: ADEL: An Automatic Detector of Energy Leaks for Smartphone Application. 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). Using Real-Time Maude to Model Check Energy Consumption Behavior. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-19249-9_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19248-2
Online ISBN: 978-3-319-19249-9
eBook Packages: Computer ScienceComputer Science (R0)