{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:45:09Z","timestamp":1743147909602,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319234038"},{"type":"electronic","value":"9783319234045"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23404-5_10","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T00:57:19Z","timestamp":1440550639000},"page":"132-149","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Runtime Verification of Expected Energy Consumption in Smartphones"],"prefix":"10.1007","author":[{"given":"Ana Rosario","family":"Espada","sequence":"first","affiliation":[]},{"given":"Mar\u00eda","family":"del Mar Gallardo","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Salmer\u00f3n","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jss.2013.10.056","volume":"90","author":"D Adalid","year":"2014","unstructured":"Adalid, D., Salmer\u00f3n, A., Gallardo, M.M., Merino, P.: Using spin for automated debugging of infinite executions of java programs. J. Syst. Softw. 90, 61\u201375 (2014)","journal-title":"J. Syst. Softw."},{"key":"10_CR2","unstructured":"Android Open Source Project: logcat. http:\/\/developer.android.com\/tools\/help\/logcat.html"},{"key":"10_CR3","unstructured":"Android Open Source Project: UIAutomatorViewer. http:\/\/developer.android.com\/training\/testing\/ui-testing\/index.html"},{"issue":"3","key":"10_CR4","doi-asserted-by":"publisher","first-page":"153","DOI":"10.3103\/S0146411608030073","volume":"42","author":"A Baums","year":"2008","unstructured":"Baums, A., Zaznova, N.: Power optimization of embedded real-time systems and their adaptability. Autom. Control Comput. Sci. 42(3), 153\u2013162 (2008). http:\/\/dx.doi.org\/10.3103\/S0146411608030073","journal-title":"Autom. Control Comput. Sci."},{"key":"10_CR5","unstructured":"Chandra, R., Fatemieh, O., Moinzadeh, P., Thekkath, C.A., Xie, Y.: End-to-end energy management of mobile devices. Technical report MSR-TR-2013-69, Microsoft, July 2013. http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=198163"},{"key":"10_CR6","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-06784-0","volume-title":"Duration Calculus - A Formal Approach to Real-Time Systems","author":"Z Chaochen","year":"2004","unstructured":"Chaochen, Z., Hansen, M.R.: Duration Calculus - A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). http:\/\/dx.doi.org\/10.1007\/978-3-662-06784-0"},{"key":"10_CR7","series-title":"Electronic Proceedings in Theoretical Computer Science","first-page":"7","volume-title":"Proceedings Tenth Workshop on Model Based Testing","author":"AR Espada","year":"2015","unstructured":"Espada, A.R., Gallardo, M.M., Salmer\u00f3n, A., Merino, P.: Using model checking to generate test cases for android applications. In: Pakulin, N., Petrenko, A.K., Schlingloff, B.H. (eds.) Proceedings Tenth Workshop on Model Based Testing. Electronic Proceedings in Theoretical Computer Science, vol. 180, pp. 7\u201321. Open Publishing Association, Amsterdam (2015)"},{"key":"10_CR8","unstructured":"Espada, A.R., Gallardo, M.M., Adalid, D.: Dragonfly: encapsulating android for instrumentation. In: Proceedings of the XIII Jornadas de Programaci\u00f3n y Lenguajes (PROLE 2013) (2013)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Liu, Y., Xu, C., Cheung, S.C.: Characterizing and detecting performance bugs for smartphone applications. In: Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pp. 1013\u20131024. ACM, New York (2014). http:\/\/doi.acm.org\/10.1145\/2568225.2568229","DOI":"10.1145\/2568225.2568229"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-16164-3_4","volume-title":"Model Checking Software","author":"P Merino","year":"2010","unstructured":"Merino, P., Salmer\u00f3n, A.: Combining SPIN with ns-2 for protocol optimization. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 40\u201357. Springer, Heidelberg (2010)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Metri, G., Shi, W., Brockmeyer, M.: Energy-efficiency comparison of mobile platforms and applications: a quantitative approach. In: Proceedings of the 16th International Workshop on Mobile Computing Systems and Applications, HotMobile 2015, pp. 39\u201344. ACM, New York (2015). http:\/\/doi.acm.org\/10.1145\/2699343.2699358","DOI":"10.1145\/2699343.2699358"},{"key":"10_CR12","unstructured":"Microsoft: Eloupe project. http:\/\/research.microsoft.com\/en-us\/projects\/eloupe\/"},{"key":"10_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-12544-2_1","volume-title":"Complex Systems Design\u00a0&\u00a0Management Asia","author":"S Nakajima","year":"2015","unstructured":"Nakajima, S.: Model checking of energy consumption behavior. In: Cardin, M.A., Krob, D., Lui, P.C., Tan, Y.H., Wood, K. (eds.) Complex Systems Design\u00a0&\u00a0Management Asia, pp. 3\u201314. Springer International Publishing, Switzerland (2015). http:\/\/dx.doi.org\/10.1007\/978-3-319-12544-2_1"},{"key":"10_CR14","unstructured":"Oracle: Java Debug Interface. http:\/\/docs.oracle.com\/javase\/6\/docs\/jdk\/api\/jpda\/jdi\/index.html"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Pathak, A., Hu, Y.C., Zhang, M.: Bootstrapping energy debugging on smartphones: a first look at energy bugs in mobile devices. In: Proceedings of the 10th ACM Workshop on Hot Topics in Networks, HotNets-X, pp. 5:1\u20135:6. ACM, New York (2011). http:\/\/doi.acm.org\/10.1145\/2070562.2070567","DOI":"10.1145\/2070562.2070567"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Pathak, A., Jindal, A., Hu, Y.C., Midkiff, S.P.: What is keeping my phone awake?: characterizing and detecting no-sleep energy bugs in smartphone apps. In: Proceedings of the 10th International Conference on Mobile Systems, Applications, and Services, MobiSys 2012, pp. 267\u2013280. ACM, New York (2012). http:\/\/doi.acm.org\/10.1145\/2307636.2307661","DOI":"10.1145\/2307636.2307661"},{"issue":"1","key":"10_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1177\/0037549714557054","volume":"91","author":"A Salmer\u00f3n","year":"2015","unstructured":"Salmer\u00f3n, A., Merino, P.: Integrating model checking and simulation for protocol optimization. Simulation 91(1), 3\u201325 (2015). http:\/\/dx.doi.org\/10.1177\/0037549714557054","journal-title":"Simulation"},{"key":"10_CR18","unstructured":"Schmitt, P.H., Werner, F.: Model checking for energy efficient scheduling in wireless sensor networks. In: Technical report (2007)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Wang, C., Yan, F., Guo, Y., Chen, X.: Power estimation for mobile applications with profile-driven battery traces. In: 2013 IEEE International Symposium on Low Power Electronics and Design (ISLPED), pp. 120\u2013125, September 2013","DOI":"10.1109\/ISLPED.2013.6629277"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-24485-8_35","volume-title":"Model Driven Engineering Languages and Systems","author":"C Wilke","year":"2011","unstructured":"Wilke, C., G\u00f6tz, S., Reimann, J., A\u00dfmann, U.: Vision paper: towards model-based energy testing. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 480\u2013489. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-24485-8_35"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Xia, M., He, W., Liu, X., Liu, J.: Why application errors drain battery easily?: a study of memory leaks in smartphone apps. In: Proceedings of the Workshop on Power-Aware Computing and Systems, HotPower 2013, pp. 2:1\u20132:5. ACM, New York (2013). http:\/\/doi.acm.org\/10.1145\/2525526.2525846","DOI":"10.1145\/2525526.2525846"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Zhang, J., Musa, A., Le, W.: A comparison of energy bugs for smartphoneplatforms. In: 2013 1st International Workshop on the Engineering of Mobile-Enabled Systems (MOBS), pp. 25\u201330, May 2013","DOI":"10.1109\/MOBS.2013.6614219"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L., Gordon, M.S., Dick, R.P., Mao, Z.M., Dinda, P., Yang, L.: Adel: an automatic detector of energy leaks for smartphone applications. In: Proceedings of the Eighth IEEE\/ACM\/IFIP International Conference on Hardware\/Software Codesign and System Synthesis, CODES+ISSS 2012, pp. 363\u2013372. ACM, New York (2012). http:\/\/doi.acm.org\/10.1145\/2380445.2380503","DOI":"10.1145\/2380445.2380503"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23404-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T08:14:27Z","timestamp":1676967267000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23404-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319234038","9783319234045"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23404-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}