Title
A model-based framework for software portability and verification in embedded power management systems.
Abstract
Run-Time Management (RTM) systems are used in embedded systems to dynamically adapt hardware performance to minimise energy consumption. A significant challenge is that RTM software can require laborious manual adjustment across different hardware platforms due to the diversity of architecture characteristics. Model-driven development offers the potential to simplify the management of platform diversity by shifting the focus away from hand-written platform-specific code to platform-independent models from which platform-specific implementations are automatically generated. Furthermore, the use of formal verification provides the means to ensure that implementations are correct-by-construction. In this paper, we present a framework for automatic generation of RTM implementations from platform-independent formal models. The methodology in designing the RTM systems uses a high-level mathematical language, Event-B, which can describe systems at different abstraction levels. A code generation tool is used to translate platform-independent Event-B RTM models to platform-specific implementations in C. Formal verification is used to ensure correctness of the Event-B models. The portability offered by our methodology is validated by modelling a Reinforcement Learning (RL) based RTM for two embedded applications and generating implementations for three different platforms (ARM Cortex-A8, A7 and A15) that all achieve energy savings on the respective platforms.
Year
DOI
Venue
2018
10.1016/j.sysarc.2017.12.001
Journal of Systems Architecture
Keywords
Field
DocType
Run-Time Management,Code generation,Formal methods,Verification
Power management,Computer science,Correctness,Implementation,Real-time computing,Software,Software portability,Energy consumption,Formal verification,Reinforcement learning,Embedded system
Journal
Volume
ISSN
Citations 
82
1383-7621
3
PageRank 
References 
Authors
0.41
14
7