Reachability Analysis of Cost-Reward Timed Automata for Energy Efficiency Scheduling.

As the ongoing scaling of semiconductor technology causing severe increase of on-chip power density in microprocessors, this leads for urgent requirement for power management during each level of computer system design. In this paper, we describe an approach for solving the general class of energy optimal task graph scheduling problems using cost-reward timed automata. We propose a formal technique based on model checking using extended timed automata to solve the processor frequency assignment problem in an energy-constrained multitasking system. To handle the problem of "state space explosion" in symbolic model checking, we also provide an efficient zone-based algorithm for minimum-cost reachability. Our approach is capable of finding efficient solutions under various constraints and applicable to other problem variants as well. Experimental results demonstrate the usefulness and effectiveness of our approach.