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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This is one of the specifications which is given as an example of a non-executable specification in [15].
- 2.
- 3.
See, https://www3.hhu.de/stups/prob/index.php/Tips:_Writing_Models_for_ProB for more details.
References
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
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
AT&T Labs-Research. Graphviz - open source graph drawing software. http://www.research.att.com/sw/tools/graphviz/
B-Core (UK) Ltd, Oxon, UK. B-Toolkit. https://github.com/edwardcrichton/BToolkit
Badeau, F., Doche-Petit, M.: Formal data validation with Event-B. CoRR, abs/1210.7039 (2012). Proceedings of DS-Event-B 2012, Kyoto
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
ClearSy: Atelier B, User, Reference Manuals. Aix-en-Provence, France (2009). http://www.atelierb.eu/
ClearSy: Data Validation & Reverse Engineering, June 2013. http://www.data-validation.fr/data-validation-reverse-engineering/
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
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
Dudeney, H.E.: Amusements in Mathematics (1917). https://www.gutenberg.org/ebooks/16713
Frhwirth, T.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009)
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
Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4–5), 767–782 (2011)
Hayes, I., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330–338 (1989)
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
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
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
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
Lamport, L.: Latex: A Document Preparation System. Addison-Wesley Longman Publishing Co., Inc., Boston (1986)
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Salt Lake City (2002)
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)
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)
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
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)
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
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)
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)
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)
Métayer, C.: AnimB: Animator of B system model in the Rodin platform (2010). http://wiki.event-b.org/index.php/AnimB
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
Murty, K.G.: Optimization Models For Decision Making, vol. 1 (2005). http://www-personal.umich.edu//~murty/books/opti_model/
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
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
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
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
Shapiro, S.C.: The jobs puzzle: a challenge for logical expressibility and automated reasoning. In: AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning (2011)
Spivey, J.M., Notation, T.Z.: A Reference Manual. Prentice-Hall, Upper Saddle River (1992)
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
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
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)