{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:59Z","timestamp":1761611159853},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Dynamic power management (DPM) refers to the use of runtime strategies in order to achieve a tradeoff between the performance and power consumption of a system and its components. We present an approach to analysing stochastic DPM strategies using probabilistic model checking as the formal framework. This is a novel application of probabilistic model checking to the area of system design. This approach allows us to obtain performance measures of strategies by automated analytical means without expensive simulations. Moreover, one can formally establish various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy.<\/jats:p>","DOI":"10.1007\/s00165-005-0062-0","type":"journal-article","created":{"date-parts":[[2005,5,18]],"date-time":"2005-05-18T13:04:36Z","timestamp":1116421476000},"page":"160-176","source":"Crossref","is-referenced-by-count":40,"title":["Using probabilistic model checking for dynamic power management"],"prefix":"10.1145","volume":"17","author":[{"given":"Gethin","family":"Norman","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandeep","family":"Shukla","sequence":"additional","affiliation":[{"name":"Bradley Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajesh","family":"Gupta","sequence":"additional","affiliation":[{"name":"Department of Information and Computer Science, University of California, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","unstructured":"[ACP] Advanced configuration and power interface website (www.acpi.info)"},{"key":"p_2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","article-title":"Reactive modules","volume":"15","author":"Alur R","year":"1999","journal-title":"Formal Methods Syst Design"},{"key":"p_3","first-page":"269","volume-title":"Alur R, Henzinger T (eds) Proceedings of 8th international conference computer aided verification (CAV'96). Lecture notes in computer science","author":"Aziz A","year":"1996"},{"issue":"3","key":"p_4","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1109\/92.845896","article-title":"A survey of design techniques for system-leveldynamic power management","volume":"8","author":"Benini L","year":"2000","journal-title":"IEEE Trans Very Large Scale Integr (TVLSI) Syst"},{"issue":"6","key":"p_5","doi-asserted-by":"crossref","first-page":"813","DOI":"10.1109\/43.766730","article-title":"Policy optimization for dynamic power management","volume":"18","author":"Benini L","year":"1999","journal-title":"IEEE Trans Comp Aided Design Integr Circuits Syst"},{"key":"p_6","first-page":"499","volume-title":"Thiagarajan P (ed) Proceedings of 15th conference foundations of software technology and theoretical computer science. Lecture notes in computer science","author":"Bd A","year":"1995"},{"key":"p_7","volume-title":"Dynamic programming and optimal control, vols 1 and 2","author":"Ber D","year":"1995"},{"key":"p_8","first-page":"780","volume-title":"Montanari U, Rolim J, Welzl E (eds) Proceedings of 27th international colloquium on automata, languages and programming (ICALP'00). Lecture notes in computer science, vol","author":"Baier C","year":"2000"},{"key":"p_9","first-page":"146","volume-title":"Baeten J, Mauw S (eds) Proceedings of 10th international conference concurrency theory (CONCUR'99). Lecture notes in computer science","author":"Baier C","year":"1999"},{"key":"p_10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5455-4","volume-title":"Dynamic power management: design techniques and CAD tools","author":"Benini L","year":"1998"},{"key":"p_11","volume-title":"Designing low-power circuits: practical recipes","author":"Benini L","year":"2001"},{"issue":"3","key":"p_12","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1287\/moor.16.3.580","article-title":"An analysis of stochastic shortest path problems","volume":"16","author":"Bertsekas D","year":"1991","journal-title":"Math Oper Res"},{"key":"p_13","first-page":"77","volume-title":"Proceedings design, automation and test in europe (DATE'99)","author":"Chung EY","year":"1999"},{"key":"p_14","volume-title":"Introduction to stochastic processes","author":"in E","year":"1975"},{"key":"p_16","volume-title":"Performance analysis of communication systems: modeling with non-markovian stochastic petri nets","author":"Ger R","year":"2000"},{"key":"p_17","first-page":"28","volume-title":"Proceedings of int. conference on computer-aided design (ICCAD'97)","author":"Hwang C-H","year":"1996"},{"key":"p_18","first-page":"96","volume-title":"Katoen J-P (ed) Proceedings of 5th International AMAST workshop on real-time and probabilistic systems (ARTS'99). Lecture notes in computer science, vol 1601","author":"Hartonas-Garmhausen V","year":"1999"},{"key":"p_19","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and probability","volume":"6","author":"Hansson H","year":"1994","journal-title":"Formal Aspects Comput"},{"key":"p_20","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Graf S, Schwartzbach M (eds) Proceedings of 6th international conference tools and algorithms for the construction and analysis of systems (TACAS","author":"Hermanns H","year":"2000"},{"key":"p_21","unstructured":"[IBM] Technical specifications of hard drive IBM Travelstar VP (www.storage.ibm.com\/storage\/oem\/data\/travvp.htm)"},{"key":"p_22","first-page":"117","volume-title":"Proceedings design automation and test conference (DATE","author":"Irani S","year":"2002"},{"key":"p_24","doi-asserted-by":"crossref","unstructured":"[KNP02a] Kwiatkowska M Norman G Pacheco A (2002) Model checking CSL until formulae with random time bounds. In: Hermanns H Segala R (eds) Proceedings of 2nd joint international workshop on process algebra and probabilistic methods performance modeling and verification (PAPM\/PROBMIV'02). Lecture notes in computer science vol 2399. Springer Berlin Heidelberg New York pp 152-168","DOI":"10.1007\/3-540-45605-8_10"},{"key":"p_25","volume-title":"Proceedings of 2nd Euro-Japanese workshop on stochastic risk modelling for finance, Insurance, Production and Reliability","author":"Kwiatkowska M","year":"2002"},{"key":"p_26","first-page":"322","volume-title":"Proceedings of 1st international conference on quantitative evaluation of systems (QEST'04)","author":"Kwiatkowska M","year":"2004"},{"key":"p_27","volume-title":"Modeling and analysis of stochastic systems","author":"Kul V","year":"1995"},{"key":"p_28","unstructured":"[Map] MapleSoft Corporation. Maple computer algebra system (www.maplesoft.com)"},{"key":"p_29","volume-title":"OnNow power management architecture for applications (msdn.microsoft.com\/library\/enus\/dndevio\/html\/onnowapp.asp)","author":"Mic","year":"1998"},{"key":"p_30","first-page":"45","volume-title":"Rosenstiel W (ed) Proceedings of 7th Annual IEEE International workshop on high level design validation and test (HLDVT'02)","author":"Norman G","year":"2002"},{"key":"p_33","first-page":"182","volume-title":"Proceedings of 35th conference design automation (DAC","author":"Paleologo G","year":"1998"},{"key":"p_34","unstructured":"[Pri] PRISM web page (www.cs.bham.ac.uk\/\u223cdxp\/prism)"},{"key":"p_35","first-page":"555","volume-title":"Proceedings of 36th conference design automation (DAC","author":"Qiu Q","year":"1999"},{"key":"p_36","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1145\/337292.337438","volume-title":"Proceedings of 37th conference design automation (DAC","author":"Qiu Q","year":"2000"},{"issue":"9","key":"p_37","doi-asserted-by":"crossref","first-page":"1200","DOI":"10.1109\/43.952737","article-title":"Stochastic modeling of a power-managed system: construction and optimization","volume":"20","author":"Qiu Q","year":"2001","journal-title":"IEEE Trans Comput Aided Design"},{"key":"p_38","volume-title":"Proceedings IEEE international conference computer-aided design","author":"Ramanathan D","year":"2000"},{"key":"p_39","first-page":"18","volume-title":"Proceedings international symposium system synthesis (ISSS","author":"Simunic T","year":"1999"},{"issue":"1","key":"p_40","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1109\/92.486080","article-title":"Predictive shutdown and other architectural techniques for energy efficient programmable computation","volume":"4","author":"Srivastava M","year":"1996","journal-title":"IEEE Trans VLSI Syst"},{"key":"p_41","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1109\/HLDVT.2001.972807","volume-title":"Proceedings IEEE workshop on high level design validation and test (HLDVT'01)","author":"Shukla S","year":"2001"},{"key":"p_42","volume-title":"Probability and Statistics with Reliability, Queuing, and Computer Science Applications","author":"Tri K","year":"2001"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0062-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0062-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0062-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:51:25Z","timestamp":1641484285000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0062-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["10.1007\/s00165-005-0062-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0062-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,8]]}}}