{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:00:05Z","timestamp":1725573605551},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540256977"},{"type":"electronic","value":"9783540320210"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11419822_5","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:35:52Z","timestamp":1292880952000},"page":"155-189","source":"Crossref","is-referenced-by-count":6,"title":["A Methodology Based on Formal Methods for Predicting the Impact of Dynamic Power Management"],"prefix":"10.1007","author":[{"given":"A.","family":"Acquaviva","sequence":"first","affiliation":[]},{"given":"A.","family":"Aldini","sequence":"additional","affiliation":[]},{"given":"M.","family":"Bernardo","sequence":"additional","affiliation":[]},{"given":"A.","family":"Bogliolo","sequence":"additional","affiliation":[]},{"given":"E.","family":"Bont\u00e0","sequence":"additional","affiliation":[]},{"given":"E.","family":"Lattanzi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","first-page":"731","DOI":"10.1109\/DSN.2004.1311944","volume-title":"Proc. of the 5th IEEE\/IFIP Int. Conf. on Dependable Systems and Networks (DSN 2004)","author":"A. Acquaviva","year":"2004","unstructured":"Acquaviva, A., Aldini, A., Bernardo, M., Bogliolo, A., Bont\u00e0, E., Lattanzi, E.: Assessing the Impact of Dynamic Power Management on the Functionality and the Performance of Battery-Powered Appliances. In: Proc. of the 5th IEEE\/IFIP Int. Conf. on Dependable Systems and Networks (DSN 2004), Firenze (Italy), pp. 731\u2013740. IEEE-CS Press, Los Alamitos (2004)"},{"key":"5_CR2","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M. Ajmone Marsan","year":"1995","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Chichester (1995)"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1109\/92.845896","volume":"8","author":"L. Benini","year":"2000","unstructured":"Benini, L., Bogliolo, A., De Micheli, G.: A Survey of Design Techniques for System-Level Dynamic Power Management. IEEE Trans. on VLSI Systems\u00a08, 299\u2013316 (2000)","journal-title":"IEEE Trans. on VLSI Systems"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1109\/43.766730","volume":"18","author":"L. Benini","year":"1999","unstructured":"Benini, L., Bogliolo, A., Paleologo, G.A., De Micheli, G.: Policy Optimization for Dynamic Power Management. IEEE Trans. on Computer Aided Design of Integrated Circuits and Systems\u00a018, 813\u2013833 (1999)","journal-title":"IEEE Trans. on Computer Aided Design of Integrated Circuits and Systems"},{"key":"5_CR5","unstructured":"Bernardo, M.: TwoTowers\u00a05.0 User Manual (2004), http:\/\/www.sti.uniurb.it\/bernardo\/twotowers\/"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0304-3975(01)00090-1","volume":"290","author":"M. Bernardo","year":"2003","unstructured":"Bernardo, M., Bravetti, M.: Performance Measure Sensitive Congruences for Markovian Process Algebras. Theoretical Computer Science\u00a0290, 117\u2013160 (2003)","journal-title":"Theoretical Computer Science"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45798-4_11","volume-title":"Performance Evaluation of Complex Systems: Techniques and Tools","author":"M. Bernardo","year":"2002","unstructured":"Bernardo, M., Donatiello, L., Ciancarini, P.: Stochastic Process Algebra: From an Algebraic Formalism to an Architectural Description Language. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol.\u00a02459, pp. 236\u2013260. Springer, Heidelberg (2002)"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"1308","DOI":"10.1109\/JPROC.2004.831207","volume":"92","author":"A. Bogliolo","year":"2004","unstructured":"Bogliolo, A., Benini, L., Lattanzi, E., De Micheli, G.: Specification and Analysis of Power-Managed Systems. Proc. of the IEEE\u00a092, 1308\u20131346 (2004)","journal-title":"Proc. of the IEEE"},{"key":"5_CR9","unstructured":"Cavada, R., Cimatti, A., Olivetti, E., Pistore, M., Roveri, M.: NuSMV\u00a02.1 User Manual (2002), http:\/\/nusmv.irst.itc.it\/"},{"key":"5_CR10","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1016\/B978-044482830-9\/50024-2","volume-title":"Handbook of Process Algebra","author":"W.R. Cleaveland","year":"2001","unstructured":"Cleaveland, W.R., Sokolsky, O.: Equivalence and Preorder Checking for Finite-State Systems. In: Handbook of Process Algebra, pp. 391\u2013424. Elsevier, Amsterdam (2001)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/BFb0023750","volume-title":"Computer-Aided Verification","author":"W.R. Cleaveland","year":"1991","unstructured":"Cleaveland, W.R.: On Automatically Explaining Bisimulation Inequivalence. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 364\u2013372. Springer, Heidelberg (1991)"},{"key":"5_CR13","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"R. Focardi","year":"1995","unstructured":"Focardi, R., Gorrieri, R.: A Classification of Security Properties. Journal of Computer Security\u00a03, 5\u201333 (1995)","journal-title":"Journal of Computer Security"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/SP.1982.10014","volume-title":"Proc. of the 3rd IEEE Symp. on Security and Privacy (SSP 1982)","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security Policy and Security Models. In: Proc. of the 3rd IEEE Symp. on Security and Privacy (SSP 1982), Oakland (CA), pp. 11\u201320. IEEE-CS Press, Los Alamitos (1982)"},{"key":"5_CR15","first-page":"874","volume-title":"Proc. of the IEEE\/ACM Int. Conf. on Computer Aided Design (ICCAD 2003)","author":"R.K. Gupta","year":"2003","unstructured":"Gupta, R.K., Irani, S., Shukla, S.K.: Formal Methods for Dynamic Power Management. In: Proc. of the IEEE\/ACM Int. Conf. on Computer Aided Design (ICCAD 2003), San Jose (CA), pp. 874\u2013882. ACM Press, New York (2003)"},{"key":"5_CR16","volume-title":"Dynamic Probabilistic Systems","author":"R.A. Howard","year":"1971","unstructured":"Howard, R.A.: Dynamic Probabilistic Systems. John Wiley & Sons, Chichester (1971)"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1109\/ICCAD.1997.643266","volume-title":"Proc. of the IEEE\/ACM Int. Conf. on Computer Aided Design (ICCAD 1997)","author":"C.-H. Hwang","year":"1997","unstructured":"Hwang, C.-H., Wu, A.: A Predictive System Shutdown Method for Energy Saving of Event-Driven Computation. In: Proc. of the IEEE\/ACM Int. Conf. on Computer Aided Design (ICCAD 1997), San Jose (CA), pp. 28\u201332. ACM Press, New York (1997)"},{"key":"5_CR18","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/HLDVT.2002.1224427","volume-title":"Proc. of the 7th IEEE Int. High-Level Design Validation and Test Workshop (HLDVT 2002)","author":"G. Norman","year":"2002","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.K., Gupta, R.K.: Formal Analysis and Validation of Continuous-Time Markov Chain Based System Level Power Management Strategies. In: Proc. of the 7th IEEE Int. High-Level Design Validation and Test Workshop (HLDVT 2002), Cannes (France), pp. 45\u201350. IEEE-CS Press, Los Alamitos (2002)"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/92.486080","volume":"4","author":"M. Srivastava","year":"1996","unstructured":"Srivastava, M., Chandrakasan, A., Brodersen, R.: Predictive System Shutdown and Other Architectural Techniques for Energy Efficient Programmable Computation. IEEE Trans. on VLSI Systems\u00a04, 42\u201355 (1996)","journal-title":"IEEE Trans. on VLSI Systems"},{"key":"5_CR21","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"W.J. Stewart","year":"1994","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"key":"5_CR22","first-page":"267","volume-title":"Computer Performance Modeling Handbook","author":"P.D. Welch","year":"1983","unstructured":"Welch, P.D.: The Statistical Analysis of Simulation Results. In: Computer Performance Modeling Handbook, pp. 267\u2013329. Academic Press, London (1983)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Mobile Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11419822_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T11:27:42Z","timestamp":1685878062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11419822_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540256977","9783540320210"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11419822_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}