Skip to main content
SpringerLink
Log in

AsmetaA: Animator for Abstract State Machines

  • Conference paper
  • First Online:
Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10817))

Abstract

In this paper, we present AsmetaA  – a graphical animator for Abstract State Machines integrated within the ASMETA framework. The execution of formal specifications through animation provides several advantages, e.g., it provides an immediate feedback about system behavior, it helps understand system evolution, and it increases the overall acceptability of formal methods.

The research reported in this paper has been partly supported by the Austrian Ministry for Transport, Innovation and Technology, the Federal Ministry of Science, Research and Economy, and the Province of Upper Austria in the frame of the COMET center SCCH.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://asmeta.sourceforge.net/.

References

  1. Arcaini, P., Gargantini, A., Riccobene, E.: NuSeen: a tool framework for the NuSMV model checker. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST), pp. 476–483 (2017)

    Google Scholar 

  2. Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E.: Visual notation and patterns for abstract state machines. In: Milazzo, P., Varró, D., Wimmer, M. (eds.) STAF 2016. LNCS, vol. 9946, pp. 163–178. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50230-4_12

    Chapter  Google Scholar 

  3. Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7

    Book  MATH  Google Scholar 

  4. Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. UCS 14(12), 1949–1983 (2008)

    Google Scholar 

  5. Haneberg, D., Junker, M., Schellhorn, G., Reif, W., Ernst, G.: Simulating a flash file system with CoreASM and eclipse. In: Informatik 2011: Informatik schafft Communities, Beiträge der 41. Jahrestagung der Gesellschaft für Informatik e.V. (GI). LNI, vol. 192, p. 355. GI (2011)

    Google Scholar 

  6. Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)

    Article  Google Scholar 

  7. Mashkoor, A., Jacquot, J.-P.: Validation of formal specifications through transformation and animation. Requir. Eng. 22(4), 433–451 (2017)

    Article  Google Scholar 

  8. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods, pp. 54–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_6

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Economics and Technology Management, Information Technology and Production, University of Bergamo, Bergamo, Italy

    Silvia Bonfanti & Angelo Gargantini

  2. Software Competence Center Hagenberg GmbH, Hagenberg, Austria

    Atif Mashkoor

  3. Johannes Kepler University Linz, Linz, Austria

    Atif Mashkoor

Authors
  1. Silvia Bonfanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Angelo Gargantini
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Atif Mashkoor
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Silvia Bonfanti .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Universität Ulm, Ulm, Germany

    Alexander Raschke

  3. University of Southampton, Southampton, United Kingdom

    Thai Son Hoang

  4. Thales Austria GmbH, Vienna, Austria

    Klaus Reichl

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bonfanti, S., Gargantini, A., Mashkoor, A. (2018). AsmetaA: Animator for Abstract State Machines. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-91271-4_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-91270-7

  • Online ISBN: 978-3-319-91271-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation