PRiME code generation plugin is a Rodin framework plugin that translates Event-B formal models to executable C/C++ code. The plugin is based on Tasking Event-B code generation plugin and has been extended to generate platform-dependent code from platform-independent formal models.
Using formal methods for automatic platform-independent code generation of run-time management
Dalvandi, M, Salehi Fathabadi, A and Butler, M (2018) Using formal methods for automatic platform-independent code generation of run-time management. University Booth at DATE 2018, Dresden, Germany. 19 - 22 Mar 2018.
Salehi Fathabadi, Asieh, Butler, Michael J., Yang, Sheng, Maeda-Nunez, Luis, Bantock, James, Al-Hashimi, Bashir M. and Merrett, Geoff V. (2018) A model-based framework for software portability and verification in embedded power management systems. Journal of Systems Architecture, 82, 12-23. (doi:10.1016/j.sysarc.2017.12.001).
The code generation plugin works with Rodin v3.3. To install a Rodin plugin you can use Eclipse Update Manager.
The code generation plugin can be installed as follows:
1- Download the plugin (PRiME-CodeGen.zip) from release section of this repository.
2- Open Rodin framework and go to Help > Install New Software...
3- Click on "Add...".
4- On "Add repository" window click on "Archive" and select the archive you downloaded in step 1.
5- Find "PRiME Code Generation 0.3.0.release" and select it.
6- Click on "Next" and continue installing the plugin.