Skip to main content
SpringerLink
Log in
Book cover

4th Refinement Workshop pp 6–33Cite as

Engineering Real Software Using Formal Methods

  • Conference paper

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

B is a formal method for the incremental development of specifications and their refinements. A prototype set of software tools supporting the method has been developed by J.-R. Abrial and BP Research. The tools support the method in the development of verifiably correct software over the spectrum of activities from early specification to coding. The platform of the toolkit is the B tool, an interactive proof assistant. The process followed using the method and tools is illustrated here in the development of a document management system. We present some early indications of the productivity of the method. It is our ultimate purpose to establish the practicality of fully applying formal techniques at all stages of software development.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R. A Formal Approach to Large Software Construction, in Mathematics of Program Construction (ed. J. L. A. van de Snepscheut ). Springer Verlag, 1989.

    Google Scholar 

  2. Abrial, J.-R. Assigning Programs to Meanings. To be published, 1991.

    Google Scholar 

  3. Dijkstra, E. W. A Discipline of Programming. Prentice Hall, 1976.

    Google Scholar 

  4. Jones, C. B. Systematic Software Development Using VDM. Prentice Hall International, 1988.

    Google Scholar 

  5. Spivey, J. M. The Z Notation a Reference Manual. Prentice Hall International, 1989.

    Google Scholar 

  6. Abrial, J.-R. B Reference Manual. Draft report, 1990.

    Google Scholar 

  7. Abrial, J.-R. A Refinement Case Study,these Proceedings.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Information Science and Engineering Branch BP Research, Sunbury Research Centre, Sunbury-on-Thames, Middx, TW16 7LN, UK

    M. K. O. Lee, P. N. Scharbach & I. H. Sørensen

Authors
  1. M. K. O. Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. N. Scharbach
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. I. H. Sørensen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, University of Glasgow, G12 8QQ, Glasgow, Scotland

    Joseph M. Morris PhD

  2. Lloyd’s Register House, Lloyd’s Register of Shipping, 29 Wellesley Road, CR0 2AJ, Croydon, Surrey, UK

    Roger C. Shaw

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lee, M.K.O., Scharbach, P.N., Sørensen, I.H. (1991). Engineering Real Software Using Formal Methods. In: Morris, J.M., Shaw, R.C. (eds) 4th Refinement Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3756-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3756-6_2

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19657-0

  • Online ISBN: 978-1-4471-3756-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation