Abstract
The B method is a well known approach to the formal specification and development of sequential computer programs. Inspired by action systems, the B method has evolved to incorporate system modelling and distributed system development. This extension is called Event-B. Even though several of the structuring mechanisms of the original B method are absent from Event-B, the desire to define and maintain structured data persists. We propose the introduction of records to Event-B for this purpose. Our approach upholds the refinement principles of Event-B by allowing the stepwise development of records too.
This research was carried out as part of the EU research project IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems) http://rodin.cs.ncl.ac.uk.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrial, J.R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
The Alloy Analyzer, http://alloy.mit.edu
Atelier, B.: http://www.atelierb.societe.com
Bicarregui, J.C., Matthews, B.M., Ritchie, B., Agerholm, S.: Investigating the integration of two formal methods. In: Proceedings of the 3rd ERCIM Workshop on Formal Methods for Industrial Critical Systems (1998)
B Core (U.K.) Ltd, http://www.b-core.com
Castagna, G.: Covariance and Contravariance: Conflict without a Cause. ACM Trans. Program. Lang. Syst. 17(3), 431–447 (1995)
Métayer, C., Abrial, J.R., Voisin, L.: Event-B Language. RODIN deliverable 3.2 (2005), http://rodin.cs.ncl.ac.uk
Naumann, D.A.: Predicate transformer semantics of a higher-order imperative language with record subtyping. Sci. Comput. Program 41(1), 1–51 (2001)
Schneider, S.: The B Method: An Introduction, Palgrave (2001)
Snook, C., Butler, M.J.: UML-B: Formal modelling and design aided by UML. ACM Trans. Software Engineering and Methodology (to appear, 2006)
Wirth, N.: The Programming Language Oberon. Softw., Pract. Exper. 18(7), 671–690 (1988)
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Evans, N., Butler, M. (2006). A Proposal for Records in Event-B. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_16
Download citation
DOI: https://doi.org/10.1007/11813040_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)