[NPK+02] Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla and Rajeev Gupta. Formal Analysis and Validation of Continuous Time Markov Chain Based System Level Power Management Strategies. In Proc. 7th Annual IEEE International Workshop on High Level Design Validation and Test (HLDVT'02), pages 45-50, OmniPress. October 2002. [ps.gz] [pdf] [bib] [Analyses probabilistic dynamic power management (DPM) strategies using CTMC models built with PRISM.]
Downloads:  ps.gz ps.gz (103 KB)  pdf pdf (67 KB)  bib bib
Notes: Further information and verification results are available from the PRISM web page.
Abstract. We have shown in the past that competitive analysis based power management strategies can be automatically analyzed for proving competitive bounds and for validating power management strategies using the SMV model checker. In this paper, we show that stochastic modelling based strategies for power management can similarly be automated for computing optimal strategies. Further, these can be analyzed for finding system parameters for satisfying probabilistic constraints. Effects of any changes in probabilistic assumptions can be easily analyzed without expensive and time consuming simulations. We demonstrate our methodology using the probabilistic model checker PRISM. We model the system using a continuous-time Markov chain, and compute strategies under varying requirements for performance. We also prove probabilistic properties of strategies using PRISM, which gives insight into individual strategies and pragmatics of their implementations. We also show the effects of changing probabilistic assumptions computed by our method and compare the results with other stochastic analysis based methods, and show that we obtain similar results in a uniform framework of probabilistic model checking.