PRiME Code Generation Tool

Run-Time Management (RTM) systems are used in embedded systems to dynamically adapt hardware performance to minimise energy consumption. A significant challenge is that the 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.

The Event-B formal modelling language can be used for specification and modelling of platform-independent RTMs. The high-level platform-independent RTM models then can be translated to platform-dependent executable code automatically.  

PRiME Code Generation tool is a Rodin* plug-in that facilitates automatic code generation of Runtime Management software from verified Event-B formal models. The tool is an extension to the existing Rodin code generation plugin (Tasking Event-B). The tool has been tailored for generation of C/C++ code that is compatible with PRiME framework. The Code Generation is available for download and use from:

https://github.com/PRiME-project/PRiME_CodeGen

————-

*Rodin is an Eclipse-based platform supporting Event-B language.