Modeling and analysis of power-aware systems

Abstract. The paper describes a formal approach for designing and rea-soning about power-constrained, timed systems. The framework is based on process algebra, a formalism that has been developed to describe and analyze communicating concurrent systems. The proposed extension al-lows the modeling of probabilistic resource failures, priorities of resource usages, and power consumption by resources within the same formalism. Thus, it is possible to model alternative power-consumption behaviors and analyze tradeoffs in their timing and other characteristics. This pa-per describes the modeling and analysis techniques, and illustrates them with examples, including a dynamic voltage-scaling algorithm.