A Methodology Based on Formal Methods for Predicting the

Abstract. One of the major issues in the design of a mobile computing device is reducing its power consumption. A commonly used technique is the adoption of a dynamic power management policy, which modifies the power consumption of the device based on certain run time con-ditions. The introduction of the dynamic power management within a battery-powered device may not be transparent, as it may alter the over-all system behavior and efficiency. Here we present a methodology that can be used in the early stages of the system design to predict the im-pact of the dynamic power management on the system functionality and performance. The predictive methodology, which relies on formal meth-ods to compare the properties of the system without and with dynamic power management, is illustrated through the application of its various phases to a simple example of power-manageable system.