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.