Formal verification of power scheduling policies for battery powered mobile systems

Ray, Sayak ; Dasgupta, Pallab ; Chakrabarti, P. P. (2006) Formal verification of power scheduling policies for battery powered mobile systems In: 2006 Annual IEEE India Conference, 15-17 September 2006, New Delhi, India.

Full text not available from this repository.

Official URL:

Related URL:


Power scheduling is a new concept of system-level dynamic power management in battery powered mobile systems. A power scheduling policy depends completely on the power request patterns of the target applications. The designer of any power scheduling policy has to guarantee that inclusion of her power scheduler in a particular set of applications would never force the system to violate any of its correctness specifications in course of power rationing. In this work, we contribute by designing quantitative temporal specification logic, named PTL, which can express system correctness properties, both functional and power related. Characteristics of this logic is that using it, one can express various power related constraints like peak power bound, temporal patterns of power consumption for a finite computation etc. along with functional temporal constraints. It supports formal performance analysis as well at the architecture level. We have also developed model checking algorithms for this logic. This would help application designers to encode temporal behaviors, both functional and power related, of the individual applications and of the system as a whole and subsequently verify whether inclusion of a power scheduler in the system ever forces any of its components to deviate from its correctness specification.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Temporal Logic; Electronic Design Automation; Power Control
ID Code:101684
Deposited On:09 Mar 2018 10:17
Last Modified:09 Mar 2018 10:17

Repository Staff Only: item control page