Skip to main content
SpringerLink
Log in

A Compact Encoding of Sequential ASMs in Event-B

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

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

Abstract

We present a translation of sequential ASMs to Event-B specifications. The translation also addresses the partial update problem, and allows a variable to be updated (consistently) in parallel. On the theoretical side, the translation highlights the intricacies of ASM rule execution in terms of Event-B semantics. On the practical side, we show on a series of examples that the Event-B encoding remains compact and is amenable to proof within Rodin as well as animation and model checking using ProB.

Part of this research by the second author was funded by a renewed Forschungspreis grant of the Humboldt Foundation in the summer of 2015.

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.

    This fact is known as the sequential ASM Thesis Gurevich proved in [14] from three natural postulates which axiomatize the underlying concept of ‘sequential algorithm’.

  2. 2.

    This is related to the circumstance that for reasons of generality arbitrary terms s, not only variables, are permitted on the left side of an assignment statement \(s:=t\). Therefore a machine may contain assignment statements \(t_1:=t\) and \(t_2:=t'\) with syntactically different \(t_i=f(t_{i,1},\ldots ,t_{i,n})\) for which however in some state S their evaluation may yield the same arguments \(eval_S(t_{1,j})=eval_S(t_{2,j})\) for all \(1 \le j \le n\) resulting in two updates \((l,eval_S(t))\) and \((l,eval_S(t'))\) to the same location \(l=(f,(eval_S(t_{1,1}),\ldots ,eval_S(t_{1,n})))\) so that the consistency condition \(eval_S(t)=eval_S(t')\) is required.

  3. 3.

    An overwrite particle in the terminology of [15].

  4. 4.

    See http://handbook.event-b.org/current/html/theorems.html.

  5. 5.

    A recent feature of ProB; it needs to be explicitly enabled via the CSE preference; it does not work across multiple events and thus cannot be applied to Fig. 2.

References

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

    Book  MATH  Google Scholar 

  2. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)

    Book  MATH  Google Scholar 

  3. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61–74. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. The Abstract State Machine Metamodel Website (2006). http://asmeta.sourceforge.net

  6. Bendisposto, J., Fritz, F., Jastram, M., Leuschel, M., Weigelt, I.: Developing Camille, a text editor for Rodin. Softw. Pract. Exp. 41(2), 189–198 (2011)

    Article  Google Scholar 

  7. Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms: correction and extension. ACM Trans. Comput. Log. 8(3), 19:1–19:32 (2008)

    MathSciNet  Google Scholar 

  8. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)

    Book  MATH  Google Scholar 

  9. Butler, M., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67–81. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Déharbe, D.: Automatic verification for a class of proof obligations with SMT-solvers. In: Proceedings ASM, pp. 217–230 (2010)

    Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Farahbod, R., et al.: The CoreASM Project. http://www.coreasm.org and https://github.com/coreasm/

  13. Foundations of Software Engineering Group, Microsoft Research. AsmL (2001). http://research.microsoft.com/foundations/AsmL/

  14. Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Trans. Comput. Log. 1(1), 77–111 (2000)

    Article  MathSciNet  Google Scholar 

  15. Gurevich, Y., Tillmann, N.: Partial updates. Theor. Comput. Sci. 336(2–3), 311–342 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

Download references

Acknowledgement

We would like to thank the reviewers of ABZ’16 for very useful feedback. The second author thanks Laurent Voisin for discussing with him during the Dagstuhl seminar Integration of Tools for Rigorous Software Construction and Analysis (September 8–13, 2013) the problem of an Asm2EventB translation. (http://drops.dagstuhl.de/opus/volltexte/2014/4358/.)

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Düsseldorf, Universitätsstr. 1, 40225, Düsseldorf, Germany

    Michael Leuschel

  2. Dipartimento di Informatica, University of Pisa, Pisa, Italy

    Egon Börger

Authors
  1. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Egon Börger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Leuschel .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Software Competence Center, Hagenberg, Austria

    Klaus-Dieter Schewe

  3. Software Competence Center, Hagenberg, Austria

    Atif Mashkoor

  4. Software Competence Center, Hagenberg, Austria

    Miklos Biro

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Leuschel, M., Börger, E. (2016). A Compact Encoding of Sequential ASMs in Event-B. In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33600-8_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33599-5

  • Online ISBN: 978-3-319-33600-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation