Abstract: Run-time management (RTM) systems [1, 2] are used in embedded systems to dynamically adapthardware performance to minimise energy consumption. An RTM system implementation is coupled with the hardware platform specifications and is implemented individually for each specific platform. A significant challenge is that RTM software can require laborious manual adjustment across differenthardware platforms due to the diversity of architecture characteristics. Hardware specifications vary from one platform to another and include a number of characteristic such as the number of supported voltage and frequency (VF) settings. Formal modelling offers the potential to simplify the management of platform diversity by shifting the focus away from handwritten platform-specific code to platform-independent models from which platform-specific implementations are automatically generated. Formal models can provide reusability and portability through abstraction and refinement. Developing RTM systems in a way that is independent of the platform specification diversity, making RTM designs portable across different platforms. Furthermore, the use of formal verification provides the means to ensure correctness.