Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Formal Model-Based Constraint Solving and Document Generation

verfasst von : Michael Leuschel

Erschienen in: Formal Methods: Foundations and Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Nächstes Kapitel Formal Testing from Natural Language in an Industrial Context
Fußnoten
1
This is one of the specifications which is given as an example of a non-executable specification in [15].
 
Literatur
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 CrossRef
2.
3.
4.
5.
Badeau, F., Doche-Petit, M.: Formal data validation with Event-B. CoRR, abs/1210.7039 (2012). Proceedings of DS-Event-B 2012, Kyoto
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 CrossRef
7.
8.
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 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.
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.
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.
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.
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.
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.
33.
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.
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
Metadaten
Titel
Formal Model-Based Constraint Solving and Document Generation
verfasst von
Michael Leuschel
Copyright-Jahr
2016
Buch
Formal Methods: Foundations and Applications

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

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

Copyright-Jahr: 2016

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

Premium Partner

    Bildnachweise