Using probabilistic model checking for dynamic power management |
| |
Authors: | Gethin Norman David Parker Marta Kwiatkowska Sandeep Shukla Rajesh Gupta |
| |
Affiliation: | (1) School of Computer Science, University of Birmingham, Birmingham, B15 2TT, UK;(2) Bradley Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, USA;(3) Department of Information and Computer Science, University of California, San Diego, USA |
| |
Abstract: | 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.Received November 2003Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke |
| |
Keywords: | Power management Formal methods Embedded systems Model checking Probabilistic model checking |
本文献已被 SpringerLink 等数据库收录! |
|