Using probabilistic model checking for dynamic power management

Gethin Norman, David Parker, Marta Kwiatkowska, S Shukla, R Gupta

Research output: Contribution to journalArticle

42 Citations (Scopus)


Dynamic power management (DPM) refers to the use of runtime strategies in order to achieve a trade-off between the performance and power consumption of a system and its components. We present an approach to analysing stochastic DPM strategies using probabilistic model checking as the formal framework. This is a novel application of probabilistic model checking to the area of system design. This approach allows us to obtain performance measures of strategies by automated analytical means without expensive simulations. Moreover, one can formally establish various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy.
Original languageEnglish
Pages (from-to)160-176
Number of pages17
JournalFormal Aspects of Computing
Issue number2
Publication statusPublished - 1 Aug 2005


  • power management
  • probabilistic model checking
  • formal methods
  • model checking
  • embedded systems


Dive into the research topics of 'Using probabilistic model checking for dynamic power management'. Together they form a unique fingerprint.

Cite this