Abstract
We present an approach to generating program code from Event-B models that is correct-by-construction. Correctness is guaranteed by the combined use of well-definedness restrictions, refinement, and assertions. By enforcing the well-definedness of the translated model, we prevent runtime errors that originate from semantic differences between the target language and Event-B, such as different interpretations of the range of integer values. Using refinement, we show that the generated code correctly implements the original Event-B model. We provide a simple yet powerful scheduling language that allows one to specify an execution sequence of the model’s guarded events where assertions are used to express properties established by the event execution sequence, which are necessary for well-definedness and refinement proofs.
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.
Similar content being viewed by others
References
Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An Open Toolset for Modelling and Reasoning in Event-B. Software Tools for Technology Transfer 12(6), 447–466 (2010)
Boström, P.: Creating Sequential Programs from Event-B Models. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 74–88. Springer, Heidelberg (2010)
Boström, P., Degerlund, F., Sere, K., Waldén, M.A.: Derivation of concurrent programs by stepwise scheduling of Event-B models. Formal Asp. Comput. 26(2), 281–303 (2014)
Edmunds, A., Butler, M.: Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In: 4th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (2011)
Fürst, A., Hoang, T.S., Basin, D., Sato, N., Miyazaki, K.: Formal System Modelling Using Abstract Data Types in Event-B. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 222–237. Springer, Heidelberg (2014)
Hoang, T.S., Abrial, J.R.: Reasoning about Liveness Properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 456–471. Springer, Heidelberg (2011)
Méry, D., Singh, N.K.: Automatic Code Generation from Event-B Models. In: Proceedings of the Second Symposium on Information and Communication Technology, SoICT 2011, pp. 179–188. ACM, New York (2011)
Wright, S.: Automatic Generation of C from Event-B. In: Workshop on Integration of Model-based Formal Methods and Tools (February 2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Fürst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K. (2014). Code Generation for Event-B. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_20
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)