Process algebraic modelling and analysis of power-aware real-time systems

A unified formal framework for designing and reasoning about power-constrained, real-time systems is described. The framework is based on process algebra, a formalism that has been developed to describe and analyse communicating, concurrent systems. The proposed extension allows the modelling of probabilistic resource failures, priorities of resource usages and power consumption by resources within the same formalism. Thus, it is possible to evaluate alternative power-consumption behaviours and tradeoffs under different real-time schedulers, resource limitations, resource failure probabilities, etc. This paper describes the modelling and analysis techniques and illustrates them with examples, including a dynamic voltage-scaling algorithm.