Embedding High-Level Formal Specifications into Applications

  • Philipp KörnerEmail author
  • Jens Bendisposto
  • Jannik Dunkelau
  • Sebastian Krings
  • Michael Leuschel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code.

In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present the enabling technology ProB 2.0, a Java API to the ProB animator and model checker. We describe several case studies that use ProB 2.0 to interact with a formal specification at runtime.



We thank Christoph Heinzen and David Geleßus for authoring and improving the presented Pac-Man application, as well as Philip Höfges for the chess model, AI and GUI. Additionally, we want to thank the many people who were involved in the development of both ProB and ProB 2.0, the Slot Tool and the ETCS Hybrid Level 3 case study.


  1. 1.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
  3. 3.
    Abrial, J.-R., Lee, M.K.O., Neilson, D.S., Scharbach, P.N., Sørensen, I.H.: The B-method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelberg (1991). Scholar
  4. 4.
    Back, R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49–68 (1981)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Back, R.-J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (2012)zbMATHGoogle Scholar
  6. 6.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Adv. Comput. 58(11), 117–148 (2003)CrossRefGoogle Scholar
  7. 7.
    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). Scholar
  8. 8.
    Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005). Scholar
  9. 9.
    Cansell, D., Méry, D.: Foundations of the B method. Comput. Inf. 22(3–4), 221–256 (2012)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997). Scholar
  11. 11.
    Carlsson, M., et al.: SICStus Prolog User’s Manual, vol. 3. Swedish Institute of Computer Science Kista, Sweden (1988)Google Scholar
  12. 12.
    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). Scholar
  13. 13.
    CENELEC. Railway Applications - Communication, signalling and processing systems - Software for railway control and protection systems. Technical report EN50128, European Standard (2011)Google Scholar
  14. 14.
    Clark, J., Bendisposto, J., Hallerstede, S., Hansen, D., Leuschel, M.: Generating Event-B specifications from algorithm descriptions. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 183–197. Springer, Cham (2016). Scholar
  15. 15.
    ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016).
  16. 16.
    Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: an extensible ASM execution engine. Fundamenta Informaticae 77(1–2), 71–103 (2007)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Fraenkel, A.: Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre. Math. Ann. 86(3), 230–237 (1922)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Fraenkel, A.A., Bar-Hillel, Y., Levy, A.: Foundations of Set Theory, vol. 67. Elsevier, Amsterdam (1973)zbMATHGoogle Scholar
  19. 19.
    Fuchs, N.E.: Specifications are (preferably) executable. Softw. Eng. J. 7(5), 323–334 (1992)CrossRefGoogle Scholar
  20. 20.
    Ghezzi, C., Kennerer, R.A.: Executing formal specifications: the ASTRAL to TRIO translation approach. In: Proceedings of the Symposium on Testing, Analysis, and Verification, TAV4, pp. 112–122. ACM (1991)Google Scholar
  21. 21.
    Gravell, A., Henderson, P.: Executing formal specifications need not be harmful. Softw. Eng. J. 11(2), 104–110 (1996)CrossRefGoogle Scholar
  22. 22.
    Hansen, D., Leuschel, M.: Translating TLA\(^+\) to B for Validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24–38. Springer, Heidelberg (2012). Scholar
  23. 23.
    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). Scholar
  24. 24.
    Hayes, I.J., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330–339 (1989)CrossRefGoogle Scholar
  25. 25.
    Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, New York (1978). Scholar
  26. 26.
    Jones, C.B.: Systematic Software Development Using VDM, vol. 2. Princeton, Citeseer (1990)zbMATHGoogle Scholar
  27. 27.
    Knuth, D.E., Moore, R.W.: An analysis of alpha-beta pruning. Artif. Intell. 6(4), 293–326 (1975)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Ladenberger, L.: Rapid creation of interactive formal prototypes for validating safety-critical systems. Ph.D. thesis (2017)Google Scholar
  29. 29.
    Ladenberger, L., Leuschel, M.: BMotionWeb: a tool for rapid creation of formal prototypes. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 403–417. Springer, Cham (2016). Scholar
  30. 30.
    Lamport, L.: Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)Google Scholar
  31. 31.
    Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative integrating tools for VDM. ACM SIGSOFT Softw. Eng. Notes 35(1), 1–6 (2010)CrossRefGoogle Scholar
  32. 32.
    Leuschel, M., Bendisposto, J.: Directed model checking for B: an evaluation and new techniques. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 1–16. Springer, Heidelberg (2011). Scholar
  33. 33.
    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). Scholar
  34. 34.
    Méry, D., Singh, N.K.: Automatic code generation from event-B models. In: Proceedings SoICT, pp. 179–188. ACM (2011)Google Scholar
  35. 35.
    Narayanasamy, S., Pokam, G., Calder, B.: BugNet: continuously recording program execution for deterministic replay debugging. In: ACM SIGARCH Computer Architecture News, vol. 33, pp. 284–295. IEEE Computer Society (2005)Google Scholar
  36. 36.
    Nielsen, C.B., Lausdahl, K., Larsen, P.G.: Combining VDM with executable code. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 266–279. Springer, Heidelberg (2012). Scholar
  37. 37.
    Nummenmaa, T.: Executable formal specifications in game development: design, validation and evolution. Ph.D. thesis (2013)Google Scholar
  38. 38.
    Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007). Scholar
  39. 39.
    Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for Event-B. STTT 19(1), 31–52 (2017)CrossRefGoogle Scholar
  40. 40.
    Schneider, D.: Constraint modelling and data validation using formal specification languages. Ph.D. thesis. Heinrich-Heine-Universität Düsseldorf (2017)Google Scholar
  41. 41.
    Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. Formal Aspects Comput. 30, 545–569 (2018)CrossRefGoogle Scholar
  42. 42.
    Spivey, J.M., Abrial, J.: The Z Notation. Prentice Hall, Hemel Hempstead (1992)Google Scholar
  43. 43.
    Vu, F.: A high-level code generator for safety critical B models. Bachelor’s thesis, Heinrich Heine Universität Düsseldorf, August 2018Google Scholar
  44. 44.
    Wahls, T., Leavens, G.T., Baker, A.L.: Executing formal specifications with concurrent constraint programming. Autom. Softw. Eng. 7(4), 315–343 (2000)CrossRefGoogle Scholar
  45. 45.
    Zenzaro, S., Gervasi, V., Soldani, J.: WebASM: an abstract state machine execution environment for the web. In: Ait Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. LNCS, vol. 8477, pp. 216–221. Springer, Heidelberg (2014). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Institut für InformatikUniversität DüsseldorfDüsseldorfGermany

Personalised recommendations