Abstract
In this chapter we consider two further state-based notations, specifically Event-B and the ASM notation. Both have similarities to Z and B, and indeed as the name suggests Event-B grew out of the B notation. Both offer more flexibility in their approach to refinement than Z and B – by adopting models closer to those in Chap. 3. One aspect of this that we discuss in this chapter is how they support refinements, and simulations, where one event or operation can be refined by several. That is, the assumption of conformality is dropped, and we discuss this below.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Texts on Event-B express the proof obligations in the sequent calculus. Without loss of generality we use implication here to be consistent with other notations in this book.
References
Abrial J-R (2010) Modeling in Event-B: system and software engineering, 1st edn. Cambridge University Press, New York
Métayer C, Abrial J-R, Voisin L (2005) Event-B language, RODIN Project Deliverable 3.2. http://rodin.cs.ncl.ac.uk/deliverables/D7.pdf. Accessed 15 June 2018
Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6):447–466
Hallerstede S (2011) On the purpose of Event-B proof obligations. Form Asp Comput 23(1):133–150
Boiten EA (2014) Introducing extra operations in refinement. Form Asp Comput 26(2):305–317
Butler M (2012) External and internal choice with event groups in Event-B. Form Asp Comput 24(4):555–567
Schneider S, Treharne H, Wehrheim H (2014) The behavioural semantics of Event-B refinement. Form Asp Comput 26(2):251–280
Börger E (2005) The ASM method for system design and analysis. A tutorial introduction. In: Gramlich Bernhard (ed) Frontiers of combining systems: 5th international workshop, FroCoS 2005, Vienna, Austria. Lecture notes in artifical intelligence, vol 3717. Springer, Berlin, pp 264–283
Börger E, Stark RF (2003) Abstract state machines: a method for high-level system design and analysis. Springer, New York
Stark RF, Börger E, Schmid J (2001) Java and the Java virtual machine: definition, verification, validation. Springer, New York
Reisig W (2008) Abstract state machines for the classroom. In: Bjørner D, Henson MC (eds) Logics of specification languages. Springer, Berlin, pp 15–46
Börger E, Raschke A (2018) Modeling companion for software practitioners. Springer, Berlin
Gurevich Y (1995) Evolving algebras 1993: lipari guide. Oxford University Press, Oxford, pp 9–36
Börger E (2003) The ASM refinement method. Form Asp Comput 15(2):237–257
Schellhorn G (2001) Verification of ASM refinements using generalized forward simulation. J Univers Comput Sci 7(11):952–979. http://www.jucs.org/jucs_7_11/verification_of_asm_refinements
Schellhorn G, Ahrendt W (1998) The WAM case study: verifying compiler correctness for prolog with KIV. In: Bibel W, Schmitt PH (eds) Automated deduction - a basis for applications, vol III. applications. Springer, Dordrecht, pp 165–194
Schellhorn G (2005) ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor Comput Sci 336(2–3):403–436
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Derrick, J., Boiten, E. (2018). State-Based Languages: Event-B and ASM. In: Refinement. Springer, Cham. https://doi.org/10.1007/978-3-319-92711-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-92711-4_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-92709-1
Online ISBN: 978-3-319-92711-4
eBook Packages: Computer ScienceComputer Science (R0)