[NPK+03] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Using Probabilistic Model Checking for Dynamic Power Management. In Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03). Technical Report DSSE-TR-2003-2, University of Southampton. April 2003. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using PRISM.]
Downloads:  ps.gz ps.gz (82 KB)  pdf pdf (256 KB)  bib bib
Notes: Further information and verification results are available from the this web page.
Abstract. We present an approach to deriving stochastic Dynamic Power Management (DPM) strategies that enables us to design both discrete time and continuous time Markov chain based strategies, in a formal and uniform framework. This is a novel application of formal model checking of probabilistic systems in the area of system design. This approach allows us to obtain expected performance measures of the derived strategies by automated analytical means without expensive simulations. Moreover, one can formally prove various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy. Comparison of various strategies under various stochastic behavioral assumptions can also be done formally without simulation. In this paper, we illustrate how we have implemented our uniform approach in the PRISM model checker framework and present results from realistic DPM scenarios based on a disk-drive example with multiple power management states.