Formal analysis and validation of continuous-time Markov chain based system level power management strategies

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. 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.