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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

SMT-Based Automatic Proof of ASM Model Refinement

verfasst von : Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Model refinement is a technique indispensable for modeling large and complex systems. Many formal specification methods share this concept which usually comes together with the definition of refinement correctness, i.e., the mathematical proof of a logical relation between an abstract model and its refined models.
Model refinement is one of the main concepts which the Abstract State Machine (ASM) formal method is built on. Proofs of correct model refinement are usually performed manually, which reduces the usability of the ASM model refinement approach. An automatic support to assist the developer in proving refinement correctness along the chain of refinement steps could be of extreme importance to improve, in practice, the adoption of ASMs.
In this paper, we present how the integration between the ASMs and Satisfiability Modulo Theories (SMT) can be used to automatically prove correctness of model refinement for the ASM method.

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
Vorheriges Kapitel Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
Nächstes Kapitel Coq Implementation of OO Verification Framework VeriJ
Fußnoten
2
Note that in concrete instances we also do not declare constants for monitored and derived functions belonging to \(\bar{f}_R ^{ nc \prime }\) and \(\bar{f}_A ^{ nc \prime }\), as they do not appear in the asserted formulas.
 
3
The tool and experimental results can be found at http://​asmeta.​sourceforge.​net/​download/​asmrefprover.​html.
 
Literatur
1.
2.
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundam. Inform. 77(1), 1–28 (2007)MathSciNetMATH
3.
Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: Proceedings of MEMOCODE 2015, pp. 80–89. IEEE (2015)
4.
5.
Arcaini, P., Gargantini, A., Riccobene, E.: Using SMT for dealing with nondeterminism in ASM-based runtime verification. In: ECEASST, vol. 70 (2014)
6.
Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from ASM models to Java code. Int. J. Softw. Tools Technol. Transf. 1–23 (2015)
7.
Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Experience 41, 155–166 (2011)CrossRef
8.
Arcaini, P., Holom, R.-M., Riccobene, E.: ASM-based formal design of an adaptivity component for a cloud system. Formal Aspects Comput. 1–29 (2016)
9.
Beierle, C., Börger, E., Durdanović, I., Glässer, U., Riccobene, E.: Refining abstract machine specifications of the steam boiler control to well documented executable code. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, pp. 52–78. Springer, Heidelberg (1996)CrossRef
10.
11.
Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Heidelberg (2014)CrossRef
12.
Börger, E.: The ASM refinement method. Formal Aspects Comput. 15(2), 237–257 (2003)CrossRefMATH
13.
Börger, E.: The Abstract State Machines method for high-level system design and analysis. In: Formal Methods: State of the Art and New Directions, pp. 79–116. Springer, London (2010)
14.
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)CrossRefMATH
15.
Derrick, J., Boiten, E.: Refinement in Z and object-Z: Foundations and Advanced Applications. Springer, London (2001)CrossRefMATH
16.
Ernst, G., Pfähler, J., Schellhorn, G., Reif, W.: Modular refinement for submachines of ASMs. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 188–203. Springer, Heidelberg (2014)CrossRef
17.
Farahbod, R., Glässer, U.: The CoreASM modeling framework. Softw. Pract. Experience 41(2), 167–178 (2011)CrossRef
18.
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2, 219–246 (1989)MathSciNetMATH
19.
Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: Part I. untimed systems. Inf. Comput. 121(2), 214–233 (1995)MathSciNetCrossRefMATH
20.
21.
Riccobene, E., Schmid, J.: Capturing requirements by abstract state machines: The light control case study. J. UCS 6(7), 597–620 (2000)
22.
Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. UCS 7(11), 952–979 (2001)MathSciNet
23.
24.
Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine, vol. 24. Springer, Heidelberg (2001)CrossRefMATH
Metadaten
Titel
SMT-Based Automatic Proof of ASM Model Refinement
verfasst von
Paolo Arcaini
Angelo Gargantini
Elvinia Riccobene
Copyright-Jahr
2016
Buch
Software Engineering and Formal Methods

Print ISBN: 978-3-319-41590-1

Electronic ISBN: 978-3-319-41591-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41591-8_17