A Case Study on Code Generation of an ERP System from Event-B

Most code generation tools for Event-B are designed for generating small, in-memory applications such as embedded controllers. In this work, we investigate whether the EventB2SQL tool (Wang and Wahls, LNCS 8702) can generate satisfactory code for the OpenBravo POS ERP (Enterprise Resource Planning) system by replacing the database core of the system with code generated from an Event-B model. We describe our methodology for generating code with EventB2SQL and enhancements to EventB2SQL that improve the performance of the generated code, and present empirical results and a user study comparing the performance of OpenBravo POS as is and with its core replaced by code generated by EventB2SQL.