Translating Event-B Machines to Database Applications

摘要

Previous work on generating implementations from Event-B models has focused on translating concrete machines that are already relatively close to code. Additionally, the generated implementations do not provide support for data persistence and for inter-operating with hand-written system components. In this work, we present the EventB-2SQL tool, which translates Event-B models to Java classes that store all model data in a relational database. Operations on sets and relations are directly translated to database queries, and Event-B carrier sets are both stored in the database and translated as generic type parameters of the generated classes. This allows developers to use objects of almost any Java class as elements of carrier sets, and to easily store these objects in the database. Additionally, using a database back-end in this manner and translating events as database transactions greatly facilitates the development of client-server and multi-threaded applications while maintaining the atomicity of events.