Deriving Minimal Models for Resource Utilization

We show how compact Resource Utilization Models (RUMs) can be extracted from concrete overly-detailed models of systems or sub-systems in order to model energy-aware software. Using the Counterexample-Guided Abstraction Refinement (CEGAR) ap-proach, along with model-checking tools, abstract models can be generated that help establish key properties relating to energy con-sumption. This approach is illustrated by the concrete example of a network manager sub-system. This work is part of an overall design methodology for energy-aware software