Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2019: Formal Methods – The Next 30 Years pp 519–535Cite as

Embedding High-Level Formal Specifications into Applications

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Cf. https://www3.hhu.de/stups/prob/index.php/Summary_of_B_Syntax.

  2. 2.

    https://github.com/bendisposto/prob2.

  3. 3.

    Available at: https://github.com/pkoerner/EventBPacman-Plugin.

  4. 4.

    On a Mac, it runs smoothly. On more powerful Linux PCs, it runs with stutters. We suspect that the socket communication is slower depending on the OS.

  5. 5.

    Available at: https://github.com/pkoerner/b-chess-example.

  6. 6.

    Available at: https://plues.github.io/en/index/.

References

  1. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  Google Scholar 

  2. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  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/BFb0020001

    Chapter  Google Scholar 

  4. Back, R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49–68 (1981)

    Article  MathSciNet  Google Scholar 

  5. Back, R.-J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (2012)

    MATH  Google Scholar 

  6. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Adv. Comput. 58(11), 117–148 (2003)

    Article  Google Scholar 

  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_1

    Chapter  Google Scholar 

  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_16

    Chapter  Google Scholar 

  9. Cansell, D., Méry, D.: Foundations of the B method. Comput. Inf. 22(3–4), 221–256 (2012)

    MathSciNet  MATH  Google Scholar 

  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/BFb0033845

    Chapter  Google Scholar 

  11. Carlsson, M., et al.: SICStus Prolog User’s Manual, vol. 3. Swedish Institute of Computer Science Kista, Sweden (1988)

    Google Scholar 

  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_13

    Chapter  Google Scholar 

  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. 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_11

    Chapter  Google Scholar 

  15. ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016). http://www.atelierb.eu/

  16. Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: an extensible ASM execution engine. Fundamenta Informaticae 77(1–2), 71–103 (2007)

    MathSciNet  MATH  Google Scholar 

  17. Fraenkel, A.: Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre. Math. Ann. 86(3), 230–237 (1922)

    Article  MathSciNet  Google Scholar 

  18. Fraenkel, A.A., Bar-Hillel, Y., Levy, A.: Foundations of Set Theory, vol. 67. Elsevier, Amsterdam (1973)

    MATH  Google Scholar 

  19. Fuchs, N.E.: Specifications are (preferably) executable. Softw. Eng. J. 7(5), 323–334 (1992)

    Article  Google Scholar 

  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. Gravell, A., Henderson, P.: Executing formal specifications need not be harmful. Softw. Eng. J. 11(2), 104–110 (1996)

    Article  Google Scholar 

  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_3

    Chapter  Google Scholar 

  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_20

    Chapter  Google Scholar 

  24. Hayes, I.J., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330–339 (1989)

    Article  Google Scholar 

  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_16

    Chapter  Google Scholar 

  26. Jones, C.B.: Systematic Software Development Using VDM, vol. 2. Princeton, Citeseer (1990)

    MATH  Google Scholar 

  27. Knuth, D.E., Moore, R.W.: An analysis of alpha-beta pruning. Artif. Intell. 6(4), 293–326 (1975)

    Article  MathSciNet  Google Scholar 

  28. Ladenberger, L.: Rapid creation of interactive formal prototypes for validating safety-critical systems. Ph.D. thesis (2017)

    Google Scholar 

  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_27

    Chapter  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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_1

    Chapter  MATH  Google Scholar 

  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_46

    Chapter  Google Scholar 

  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. 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. 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_19

    Chapter  Google Scholar 

  37. Nummenmaa, T.: Executable formal specifications in game development: design, validation and evolution. Ph.D. thesis (2013)

    Google Scholar 

  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_25

    Chapter  Google Scholar 

  39. Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for Event-B. STTT 19(1), 31–52 (2017)

    Article  Google Scholar 

  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. Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. Formal Aspects Comput. 30, 545–569 (2018)

    Article  Google Scholar 

  42. Spivey, J.M., Abrial, J.: The Z Notation. Prentice Hall, Hemel Hempstead (1992)

    Google Scholar 

  43. Vu, F.: A high-level code generator for safety critical B models. Bachelor’s thesis, Heinrich Heine Universität Düsseldorf, August 2018

    Google Scholar 

  44. Wahls, T., Leavens, G.T., Baker, A.L.: Executing formal specifications with concurrent constraint programming. Autom. Softw. Eng. 7(4), 315–343 (2000)

    Article  Google Scholar 

  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_19

    Chapter  Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Düsseldorf, Universitätsstr. 1, 40225, Düsseldorf, Germany

    Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings & Michael Leuschel

Authors
  1. Philipp Körner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jens Bendisposto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jannik Dunkelau
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sebastian Krings
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Philipp Körner .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Körner, P., Bendisposto, J., Dunkelau, J., Krings, S., Leuschel, M. (2019). Embedding High-Level Formal Specifications into Applications. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_31

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_31

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation