Advertisement

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)

Abstract

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.

Notes

Acknowledgement

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.

References

  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).  https://doi.org/10.1007/BFb0020001CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-15075-8_1CrossRefGoogle 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).  https://doi.org/10.1007/11526841_16CrossRefGoogle 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).  https://doi.org/10.1007/BFb0033845CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-40648-0_13CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-33600-8_11CrossRefGoogle Scholar
  15. 15.
    ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016). http://www.atelierb.eu/
  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).  https://doi.org/10.1007/978-3-642-30729-4_3CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-91271-4_20CrossRefGoogle 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).  https://doi.org/10.1007/978-1-4757-3472-0_16CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-41591-8_27CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-19829-8_1CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-540-45236-2_46CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-30885-7_19CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-73210-5_25CrossRefGoogle 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).  https://doi.org/10.1007/978-3-662-43652-3_19CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

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

Personalised recommendations