Skip to main content
Springer Nature Link
Log in

Formal Model-Based Constraint Solving and Document Generation

  • Conference paper
  • First Online:
Formal Methods: Foundations and Applications (SBMF 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10090))

Included in the following conference series:

Abstract

Constraint solving technology for formal models has made considerable progress in the last years, and has lead to many applications such as animation of high-level specifications, test case generation, or symbolic model checking. In this article we discuss the idea to use formal models themselves to express constraint satisfaction problems and to embed formal models as executable artefacts at runtime. As part of our work, we have developed a document generation feature, whose output is derived from such executable models. This present article has been generated using this feature, and we use the feature to showcase the suitability of formal modelling to express and solve various constraint solving benchmark examples. We conclude with current limitations and open challenges of formal model-based constraint solving.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
eBook
USD 39.99
Price excludes VAT (USA)
Softcover Book
USD 54.99
Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    This is one of the specifications which is given as an example of a non-executable specification in [15].

  2. 2.

    See https://www.ctan.org/pkg/skak.

  3. 3.

    See, https://www3.hhu.de/stups/prob/index.php/Tips:_Writing_Models_for_ProB for more details.

References

  1. Abo, R., Voisin, L.: Formal implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 221–236. Springer, Heidelberg (2014). doi:10.1007/978-3-319-05032-4_17

    Chapter  Google Scholar 

  2. Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  3. AT&T Labs-Research. Graphviz - open source graph drawing software. http://www.research.att.com/sw/tools/graphviz/

  4. B-Core (UK) Ltd, Oxon, UK. B-Toolkit. https://github.com/edwardcrichton/BToolkit

  5. Badeau, F., Doche-Petit, M.: Formal data validation with Event-B. CoRR, abs/1210.7039 (2012). Proceedings of DS-Event-B 2012, Kyoto

    Google Scholar 

  6. 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). doi:10.1007/BFb0033845

    Chapter  Google Scholar 

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

  8. ClearSy: Data Validation & Reverse Engineering, June 2013. http://www.data-validation.fr/data-validation-reverse-engineering/

  9. Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194–207. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30885-7_14

    Chapter  Google Scholar 

  10. Dobrikov, I., Leuschel, M.: Enabling analysis for event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 102–118. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33600-8_6

    Chapter  Google Scholar 

  11. Dudeney, H.E.: Amusements in Mathematics (1917). https://www.gutenberg.org/ebooks/16713

  12. Frhwirth, T.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009)

    Book  Google Scholar 

  13. Hall, A.: Integrating Z into large projects tools and techniques. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 337–337. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87603-8_26

    Chapter  Google Scholar 

  14. Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4–5), 767–782 (2011)

    MathSciNet  Google Scholar 

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

    Article  Google Scholar 

  16. Idani, A., Ledru, Y.: B for modeling secure information systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 312–318. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25423-4_20

    Chapter  Google Scholar 

  17. Krings, S., Bendisposto, J., Leuschel, M.: From failure to proof: the ProB disprover for B and Event-B. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 199–214. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22969-0_15

    Chapter  Google Scholar 

  18. Krings, S., Leuschel, M.: Proof assisted symbolic model checking for B and Event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 135–150. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33600-8_8

    Chapter  Google Scholar 

  19. Krings, S., Leuschel, M.: SMT solvers for validation of B and Event-B models. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361–375. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33693-0_23

    Chapter  Google Scholar 

  20. Lamport, L.: Latex: A Document Preparation System. Addison-Wesley Longman Publishing Co., Inc., Boston (1986)

    MATH  Google Scholar 

  21. Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Salt Lake City (2002)

    Google Scholar 

  22. Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, abs/1210.6815. Proceedings of DS-Event-B 2012, Kyoto (2012)

    Google Scholar 

  23. Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the ProB constraint solver 10 years on. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, chap. 14, pp. 427–446. Wiley ISTE, Hoboken (2014)

    Google Scholar 

  24. 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). doi:10.1007/978-3-540-45236-2_46

    Chapter  Google Scholar 

  25. Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)

    Article  Google Scholar 

  26. Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 708–723. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05089-3_45

    Chapter  Google Scholar 

  27. Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Formal Asp. Comput. 23(6), 683–709 (2011)

    Article  MathSciNet  Google Scholar 

  28. Leuschel, M., Schneider, D.: Towards B as a high-level constraint modelling language. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 101–116. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  29. Marriott, K., Nethercote, N., Rafeh, R., Stuckey, P.J., de la Banda, M.G., Wallace, M.: The design of the Zinc modelling language. Constraints 13(3), 229–267 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  30. Métayer, C.: AnimB: Animator of B system model in the Rodin platform (2010). http://wiki.event-b.org/index.php/AnimB

  31. Moreira, A.M., Hentz, C., Déharbe, D., Matos, E.C.B., Neto, J.B.S., Medeiros, V.: Verifying code generation tools for the B-method using tests: a case study. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 76–91. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21215-9_5

    Chapter  Google Scholar 

  32. Murty, K.G.: Optimization Models For Decision Making, vol. 1 (2005). http://www-personal.umich.edu//~murty/books/opti_model/

  33. Plagge, D., Leuschel, M.: Validating B, Z and TLA + Using ProB and Kodkod. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372–386. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_31

    Chapter  Google Scholar 

  34. Savary, A., Frappier, M., Leuschel, M., Lanet, J.-L.: Model-based robustness testing in Event-B using mutation. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 132–147. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22969-0_10

    Chapter  Google Scholar 

  35. Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487–495. Springer, Heidelberg (2015). doi:10.1007/978-3-319-19249-9_30

    Chapter  Google Scholar 

  36. Servat, T.: BRAMA: a new graphic animation tool for B models. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 274–276. Springer, Heidelberg (2006). doi:10.1007/11955757_28

    Chapter  Google Scholar 

  37. Shapiro, S.C.: The jobs puzzle: a challenge for logical expressibility and automated reasoning. In: AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning (2011)

    Google Scholar 

  38. Spivey, J.M., Notation, T.Z.: A Reference Manual. Prentice-Hall, Upper Saddle River (1992)

    Google Scholar 

  39. Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_49

    Chapter  Google Scholar 

  40. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999). doi:10.1007/3-540-48153-2_6

    Chapter  Google Scholar 

Download references

Acknowledgements

I would like to thank all those people who have contributed towards the development of ProB and without whom the tool would not be where it is now: Jens Bendisposto, Michael Butler, Ivaylo Dobrikov, Marc Fontaine, Fabian Fritz, Dominik Hansen, Philipp Körner, Sebastian Krings, Lukas Ladenberger, Daniel Plagge, David Schneider, Corinna Spermann, and many more. I also thank Stefan Hallerstede for feedback and discussions about this article.

Author information

Authors and Affiliations

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

    Michael Leuschel

Authors
  1. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Leuschel .

Editor information

Editors and Affiliations

  1. Universidad Federal do Rio Grande do Sul, Porto Alegre, Brazil

    Leila Ribeiro

  2. ClearSy, Aix en Provence, France

    Thierry Lecomte

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Leuschel, M. (2016). Formal Model-Based Constraint Solving and Document Generation. In: Ribeiro, L., Lecomte, T. (eds) Formal Methods: Foundations and Applications. SBMF 2016. Lecture Notes in Computer Science(), vol 10090. Springer, Cham. https://doi.org/10.1007/978-3-319-49815-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-49815-7_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-49814-0

  • Online ISBN: 978-3-319-49815-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation