Abstract
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 EventB2SQL 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157. Springer, Heidelberg (2006)
Catano, N., Rueda, C.: Matelas: A predicate calculus common formal definition for social networking. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 259–272. Springer, Heidelberg (2010)
Codd, E.F.: Recent investigations in relational data base systems. In: IFIP Congress. pp. 1017–1021 (1974)
Edmunds, A., Butler, M.: Tool support for Event-B code generation. In: WS-TBFM 2010. John Wiley and Sons, Québec (2010)
Edmunds, A., Butler, M.: Tasking Event-B: An extension to Event-B for generating concurrent code. In: Programming Language Approaches to Concurrency and Communication-Centric Software PLACES. Springer, Saarbrucken (2011)
Méry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the Second SoICT, SoICT 2011. ACM, Hanoi (2011)
Wang, Q., Wahls, T.: The EventB2SQL tool – Rodin plugin and usage example (2013), http://users.dickinson.edu/~wahlst/eventb2sql/eventb2sql.html
Wright, S.: Automatic generation of C from Event-B. In: Workshop on IM_FMT. Springer, Nantes (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Wang, Q., Wahls, T. (2014). Translating Event-B Machines to Database Applications. In: Giannakopoulou, D., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science, vol 8702. Springer, Cham. https://doi.org/10.1007/978-3-319-10431-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-10431-7_19
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10430-0
Online ISBN: 978-3-319-10431-7
eBook Packages: Computer ScienceComputer Science (R0)