Abstract
Within high-level specification languages such as B, code is refined in many steps until a small “implementable” subset of the language is reached. Then, code generators are used, targeting programming languages such as C or Ada.
We aim to diminish the number of refinement steps needed, by providing an improved code generator. Indeed, many high-level operations and data types, such as sets, can be dealt with in programming languages such as Java and C++. We present a code generator for B named B2Program with two distinct features. Firstly, it targets multiple (high-level) languages via a template-based approach to compilation. In addition to flexibility, this also enables one to safeguard against errors in the individual compilers and standard libraries, by generating multiple implementations of the same formal model. Secondly, it supports higher-level constructs compared to existing code generators. This enables new uses of formal models, as prototypes, demonstrators or simply as very high-level programming languages, by directly embedding formal models as components into software systems. In the article, we discuss the implementation of our code generator, evaluate it using B models taken from literature and compare its performance with simulation in ProB.
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
Similar content being viewed by others
Notes
- 1.
Available at: https://github.com/favu100/b2program.
- 2.
SIL stands for Safety Integrity Level. SIL-4 is the highest level of integrity for railway systems. See https://en.wikipedia.org/wiki/Safety_integrity_level.
- 3.
- 4.
Note that assignment does not copy the data structure; it copies just the reference.
- 5.
Several benchmarks ran slower than simulation with ProB.
- 6.
But note that the timings reported in [32] are incorrect. In our experiments the EventB2Java generated code seems to be about twice as fast as execution with ProB, taking in the order of 8.15 s to sort 1000 elements. In [32] it is reported that sorting a 100,000 element array takes 0.023 s, and a 200,000 element array 0.028 s which is impossible using a quadratic insertion sort.
References
Abrial, J., Hoare, A.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Sethi, R., Aho, A.V., Lam, M.S.: The structure of a compiler. In: Compilers Principles, Techniques & Tools, 2nd edn. Addison Wesley, Boston (1986)
Backhouse, R., Gibbons, J.: Generic Programming. Springer, Heidelberg (2003)
Bagwell, P.: Ideal Hash Trees. Es Grands Champs, 1195 (2001)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Bonfanti, S., Carissoni, M., Gargantini, A., Mashkoor, A.: Asm2C++: a tool for code generation from abstract state machines to arduino. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 295–301. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_21
Bonichon, R., Déharbe, D., Lecomte, T., Medeiros, V.: LLVM-based code generation for B. In: Braga, C., Martí-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 1–16. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15075-8_1
Cataño, N., Rivera, V.: EventB2Java: a code generator for event-B. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 166–171. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_13
ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016). http://www.atelierb.eu/
Dollé, D., Essamé, D., Falampin, J.: B dans le transport ferroviaire. L’expérience de Siemens Transportation Systems. Technique et Science Informatiques 22(1), 11–32 (2003)
Edmunds, A.: Templates for event-B code generation. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 284–289. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_25
Essamé, D., Dollé, D.: B in large-scale projects: the canarsie line CBTC experience. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 252–254. Springer, Heidelberg (2006). https://doi.org/10.1007/11955757_21
Fürst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323–338. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_20
Granlund, T.: GNU MP. The GNU Multiple Precision Arithmetic Library, vol. 2, no. 2 (1996)
Hansen, D., Leuschel, M.: Translating B to TLA + for validation with TLC. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 40–55. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_4
Hansen, D., et al.: Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 292–306. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_20
Hickey, R.: The Clojure programming language. In: Proceedings of DLS. ACM (2008)
Hunt, A., Thomas, D.: The evils of duplication. In: The Pragmatic Programmer: From Journeyman to Master, p. 26. The Pragmatic Bookshelf (1999)
Jørgensen, P.W.V., Larsen, M., Couto, L.D.: A code generation platform for VDM. In: Battle, N., Fitzgerald, J. (eds.) Proceedings of the 12th Overture Workshop. School of Computing Science, Newcastle University, UK, Technical report CS-TR-1446, January 2015
Kaplan, H.: Persistent data structures. In: Handbook of Data Structures and Applications (2004)
Krings, S.: Towards infinite-state symbolic model checking for B and event-B. Ph.D. thesis, Heinrich Heine Universität Düsseldorf, August 2017
Körner, P., Bendisposto, J., Dunkelau, J., Krings, S., Leuschel, M.: Embedding high-level formal specifications into applications. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 519–535. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_31
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, POPL, pp. 42–54. ACM Press (2006)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exper. 48(12), 2350–2379 (2018)
Méry, D., Singh, N.K.: Automatic code generation from event-B models. In: Proceedings SoICT 2011, pp. 179–188. ACM ICPS (2011)
Parr, T.: Enforcing Strict Model-View Separation in Template Engines. https://www.cs.usfca.edu/~parrt/papers/mvc.templates.pdf. Accessed 14 May 2019
Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12, 9–21 (2007)
Puente, J.P.B.: Persistence for the masses: RRB-vectors in a systems language. In: Proceedings of ACM Programming Languages, vol. 1, no. ICFP, pp. 16:1–16:28 (2017)
Requet, A.: BART: a tool for automatic refinement. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 345–345. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_33
Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for Event-B. STTT 19(1), 31–52 (2017)
Voisinet, J.-C.: JBTools: an experimental platform for the formal B method. In: Proceedings of the Inaugural International Symposium on Principles and Practice of Programming in Java, pp. 137–139 (2002)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Vu, F., Hansen, D., Körner, P., Leuschel, M. (2019). A Multi-target Code Generator for High-Level B. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-34968-4_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34967-7
Online ISBN: 978-3-030-34968-4
eBook Packages: Computer ScienceComputer Science (R0)