[KNP05c] Marta Kwiatkowska, Gethin Norman and David Parker. Probabilistic Model Checking and Power-Aware Computing. In In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), pages 6-9. September 2005. [ps.gz] [pdf] [bib] [Applies PRISM to the analysis of power-aware systems: dynamic power management and dynamic voltage scaling.]
Downloads:  ps.gz ps.gz (36 KB)  pdf pdf (103 KB)  bib bib
Abstract. Power-aware computing aims either to maximise the performance of a system under certain constraints on its power consumption and dissipation or, dually, to reduce power consumption in order to meet desired performance or throughput targets. This area is currently gaining importance due to the increasing usage of portable, mobile and hand-held electronic devices. In this paper we illustrate the applicability of probabilistic model checking, a formal verification technique for the analysis of systems which exhibit stochastic behaviour, to the field of power-aware computing. We use the probabilistic model checking tool PRISM on two case studies in this application domain: dynamic power management and dynamic voltage scaling.