Abstract
This paper introduces B, a mathematically based method and a computer based tool-kit for software engineering. The B-Method provides a notation and a method for the formal specification and design of software. Incremental construction of layered software as well as incremental mathematical verification have been guiding principles in its development. The method uses a ‘pseudo’ programming language Abstract Machine Notation as the language for design as well as for specification within the software process. AMN is based on an extension of Dijkstra’s guarded command language, with built-in structuring mechanisms for the construction of larger systems. The B-Method is explained in The B-Book [Abrial, 1997].The B-Toolkit supports the method over the spectrum of activities from specification through design and implementation into maintenance. The B-Toolkit comprises automatic and interactive theorem-proving assistants, and a set of software development tools: an AMN syntax & type checker, a specification animator and code generators, and promotes an object oriented approach at all stages of development. All tools are integrated into a window-based development environment. The B-Toolkit is developed and sold by B-Core.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J-R., “B-Tool Reference Manual”, BP International Ltd, 1991 (available from B-Core).
Abrial, J-R. et al, “B-Technology Technical Overview”, B-Core(UK) Ltd. 1993.
Abrial, J-R., “The B-Book: Assigning Programs to Meaning”,Cambridge University Press, 1997.
Behm, P., Benoit. P., Faivre. A., Meynadier, J-M., “Meteor: A Successful Application of B in a Large Project”.
Blarney, W., McNeil, I., “Productivity Gains Through the Use of the B-Method”, ITRU/273, BP Internal Report, 1991.
Carnot, M., DaSilva, C., Dehbonei, B., Mejia, F., “Error-free Software Development for Critical Systems Using the B-Methodology”, in Proceedings of the Third IEEE International Conference on Software Reliability Engineering, October 92, North Carolina, USA.
Dijkstra, E.W., “A Discipline of Programming”,Prentice Hall, 1976. Gries
He, J. et al., “Data Refinement Refined”, LNCS volume 213, Springer-Verlag, 1986.
Ifill, W., “The Use of B to Specify, Design and Verify Hardware”, HIS Conference, November 1999.
Jones, C.B., “Systematic Software Development Using VDM”, Prentice Hall, Englewood Cliffs, NJ 1986.
Lano, K., “The B Language and Method”. Springer-Verlag, 1996.
Lee, M.K.O., Scharbach, P.N., Sørensen,I.H., “Engineering Real Software Using Formal Methods”, in Proceedings of the Fourth Refinement Workshop, Springer-Verlag, 1991.
Morgan, C.C., “Programming From Specifications”, Prentice Hall, 1990.
Sørensen, I.H, “Using B to Specify, Verify and Design Hardware Circuits”, LNCS 1493, Springer-Verlag.
Spivey, J.M., “Understanding Z”, Cambridge University Press, 1988.
Wing J.M., Woodcock, J., Davies, J.(Eds.) “FM’99 — Formal Methods”, LNCS 1708, Springer, 1999.
Wordsworth, J.B., “Software Engineering with B”, Addison-Wesley, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Sorensen, I., Neilson, D. (2001). B: Towards Zero Defect Software. In: Winter, V.L., Bhattacharya, S. (eds) High Integrity Software. The Kluwer International Series in Engineering and Computer Science, vol 577. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1391-9_2
Download citation
DOI: https://doi.org/10.1007/978-1-4615-1391-9_2
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-5530-4
Online ISBN: 978-1-4615-1391-9
eBook Packages: Springer Book Archive