Abstract
Refining a B specification into an implementation can be a complex and time consuming process. This process can usually be separated in two distinct parts: the specification part, where the refinement is used to introduce new properties and specification details, and the implementation, where refinement is used to convert a detailed B specification into a B0 implementation. The first part requires human interaction, since it corresponds to writing the specification. However, the implementation part is more mechanical, and usually corresponds to apply known refinement schemes.
This work has been funded by french ”Agence Nationale de la Recherche” ANR-06-SETI-015.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Requet, A. (2008). BART: A Tool for Automatic Refinement. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-87603-8_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87602-1
Online ISBN: 978-3-540-87603-8
eBook Packages: Computer ScienceComputer Science (R0)