Formal Verification of Power Scheduling Policies for Battery Powered Mobile Systems

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