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 |
Name | Order | Citations | PageRank |
---|---|---|---|
Asieh Salehi Fathabadi | 1 | 48 | 8.14 |
Michael Butler | 2 | 1768 | 104.74 |
Sheng Yang | 3 | 74 | 6.75 |
luis alfonso maedanunez | 4 | 15 | 1.39 |
James R. B. Bantock | 5 | 3 | 0.41 |
Bashir M. Al-Hashimi | 6 | 1339 | 112.57 |
Geoff V. Merrett | 7 | 16 | 1.49 |