{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T15:25:55Z","timestamp":1725809155393},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319125435"},{"type":"electronic","value":"9783319125442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-12544-2_1","type":"book-chapter","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T15:01:55Z","timestamp":1415977315000},"page":"3-14","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking of Energy Consumption Behavior"],"prefix":"10.1007","author":[{"given":"Shin","family":"Nakajima","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Android, \n                  \n                    http:\/\/developer.android.com"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-56922-7_16","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: Computing Accumulated Delays in Real-Time System. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 181\u2013193. Springer, Heidelberg (1993)"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A Really Temporal Logic. J. Accoc. Comp. Machin.\u00a041(1), 181\u2013204 (1994)","journal-title":"J. Accoc. Comp. Machin."},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"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.\u00a0138, 3\u201324 (1995)","journal-title":"Theor. Comp. Sci."},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2001","unstructured":"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.\u00a02034, pp. 49\u201362. Springer, Heidelberg (2001)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G. Behrmann","year":"2001","unstructured":"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.\u00a02034, pp. 147\u2013161. Springer, Heidelberg (2001)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed Automata with Observers under Energy Constraints. In: Proc. HSCC 2010 (2010)","DOI":"10.1145\/1755952.1755963"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-28717-6_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Li, G., B\u00f8gsted Poulsen, D., Stainer, A.: Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 168\u2013182. Springer, Heidelberg (2012)"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Processing Letters\u00a040, 269\u2013276 (1991)","journal-title":"Information Processing Letters"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, 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.\u00a06919, pp. 80\u201396. Springer, Heidelberg (2011)"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.ic.2006.08.003","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri, S., Lazi\u0107, R., Nowak, D.: On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. Information and Computation\u00a0205(1), 2\u201324 (2007)","journal-title":"Information and Computation"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s00165-008-0082-7","volume":"20","author":"R. Meyer","year":"2008","unstructured":"Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model Checking Duration Calculus: a practical approach. Formal Aspects of Computing\u00a020, 481\u2013505 (2008)","journal-title":"Formal Aspects of Computing"},{"key":"1_CR13","unstructured":"Nakajima, S.: Model-based Power Consumption Analysis of Smartphone Applications. In: Proc. ACES-MB 2013 (2013)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Nakajima, S.: Everlasting Challenges with the OBJ Language Family. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Futatsugi Festschrift. LNCS, vol.\u00a08373, pp. 478\u2013493. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54624-2_24"},{"key":"1_CR15","unstructured":"Nakajima, S.: Platform-Dependence in Model-based Energy Consumption Analysis of Smartphone Applications. NII Technical Report (2014)"},{"issue":"1-2","key":"1_CR16","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and Pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation\u00a020(1-2), 161\u2013196 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"4","key":"1_CR17","first-page":"5","volume":"176","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and Completeness for Real-Time Maude. ENTCS\u00a0176(4), 5\u201327 (2007)","journal-title":"ENTCS"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J. Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some Recent Results in Metric Temporal Logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 1\u201313. Springer, Heidelberg (2008)"},{"key":"1_CR19","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: Proc. Hotnets 2011 (2011)","DOI":"10.1145\/2070562.2070567"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2168836.2168841"},{"issue":"3","key":"1_CR21","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. Statistical Probablistic Model Checking. J. STTT\u00a08(3), 216\u2013228 (2006)","journal-title":"J. STTT"},{"key":"1_CR22","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 Engery Leaks for Smartphone Applications. In: Proc. CODES+ISSS 2012 (2012)","DOI":"10.1145\/2380445.2380503"}],"container-title":["Complex Systems Design & Management Asia"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12544-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T13:53:33Z","timestamp":1559051613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12544-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319125435","9783319125442"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12544-2_1","relation":{},"subject":[],"published":{"date-parts":[[2015]]}}}