Top

Published in:

2016 | OriginalPaper | Chapter

Formal Model-Based Constraint Solving and Document Generation

Author : Michael Leuschel

Published in: Formal Methods: Foundations and Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter Formal Testing from Natural Language in an Industrial Context

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

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

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

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 CrossRef

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

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 CrossRef

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 CrossRef

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 CrossRef

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

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 CrossRef

14.

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

15.

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

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

20.

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

21.

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

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)

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)

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 CrossRef

25.

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

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 CrossRef

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

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

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

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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)

38.

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

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 CrossRef

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 CrossRef

Title: Formal Model-Based Constraint Solving and Document Generation
Author: Michael Leuschel
Publisher: Springer International Publishing
Book: Formal Methods: Foundations and Applications
Print ISBN: 978-3-319-49814-0

Electronic ISBN: 978-3-319-49815-7

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-49815-7_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner