Using probabilistic model checking for dynamic power management

Research output: Contribution to journal › Article

Standard

Using probabilistic model checking for dynamic power management. / Norman, Gethin; Parker, David; Kwiatkowska, Marta; Shukla, S; Gupta, R.

In: Formal Aspects of Computing, Vol. 17, No. 2, 01.08.2005, p. 160-176.

Research output: Contribution to journal › Article

Harvard

Norman, G, Parker, D, Kwiatkowska, M, Shukla, S & Gupta, R 2005, 'Using probabilistic model checking for dynamic power management', Formal Aspects of Computing, vol. 17, no. 2, pp. 160-176. https://doi.org/10.1007/s00165-005-0062-0

APA

Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., & Gupta, R. (2005). Using probabilistic model checking for dynamic power management. Formal Aspects of Computing, 17(2), 160-176. https://doi.org/10.1007/s00165-005-0062-0

Vancouver

Norman G, Parker D, Kwiatkowska M, Shukla S, Gupta R. Using probabilistic model checking for dynamic power management. Formal Aspects of Computing. 2005 Aug 1;17(2):160-176. https://doi.org/10.1007/s00165-005-0062-0

Author

Norman, Gethin ; Parker, David ; Kwiatkowska, Marta ; Shukla, S ; Gupta, R. / Using probabilistic model checking for dynamic power management. In: Formal Aspects of Computing. 2005 ; Vol. 17, No. 2. pp. 160-176.

Bibtex

@article{6b6f9b6bdec74891bf60005b78206e13,
title = "Using probabilistic model checking for dynamic power management",
abstract = "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.",
keywords = "power management, probabilistic model checking, formal methods, model checking, embedded systems",
author = "Gethin Norman and David Parker and Marta Kwiatkowska and S Shukla and R Gupta",
year = "2005",
month = aug,
day = "1",
doi = "10.1007/s00165-005-0062-0",
language = "English",
volume = "17",
pages = "160--176",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer",
number = "2",

}

RIS

TY - JOUR

T1 - Using probabilistic model checking for dynamic power management

AU - Norman, Gethin

AU - Parker, David

AU - Kwiatkowska, Marta

AU - Shukla, S

AU - Gupta, R

PY - 2005/8/1

Y1 - 2005/8/1

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

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

KW - power management

KW - probabilistic model checking

KW - formal methods

KW - model checking

KW - embedded systems

UR - http://www.scopus.com/inward/record.url?scp=23844461782&partnerID=8YFLogxK

U2 - 10.1007/s00165-005-0062-0

DO - 10.1007/s00165-005-0062-0

M3 - Article

VL - 17

SP - 160

EP - 176

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 2

ER -