Skip to main content
SpringerLink
Log in

Model Based Refinement and the Tools of Tomorrow

  • Conference paper
Abstract State Machines, B and Z (ABZ 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5238))

Included in the following conference series:

Abstract

The ingredients of typical model based development via refinement are re-examined, and some well known frameworks are reviewed in that light, drawing out commonalities and differences. It is observed that alterations in semantics take place de facto due to applications pressures and for other reasons. This leads to a perspective on tools for such methods in which the proof obligations become programmable and/or configurable, permitting easier co-operation between techniques and interaction with an Evidential Tool Bus. This is of intrinsic interest, and also relevant to the Verification Grand Challenge.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. C.U.P (1998)

    Google Scholar 

  2. Rushby, J.: Harnessing Disruptive Innovation in Formal Verification. In: Proc. IEEE SEFM 2006, pp. 21–28. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  3. Jones, C., O’Hearne, P., Woodcock, J.: Verified Software: A Grand Challenge. IEEE Computer 39(4), 93–95 (2006)

    Google Scholar 

  4. Woodcock, J.: First Steps in the The Verified Software Grand Challenge. IEEE Computer 39(10), 57–64 (2006)

    Google Scholar 

  5. Woodcock, J., Banach, R.: The Verification Grand Challenge. Communications of the Computer Scociety of India (May 2007)

    Google Scholar 

  6. Börger, E., Stärk, R.: Abstract State Machines. A Method for High Level System Design and Analysis. Springer, Heidelberg (2003)

    Google Scholar 

  7. ISO/IEC 13568: Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics: International Standard (2002), http://www.iso.org/iso/en/ittf/PubliclyAvailableStandards/c021573_I SO_IEC_13568_2002(E).zip

    Google Scholar 

  8. Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. PHI (1996)

    Google Scholar 

  9. Derrick, J., Boiten, E.: Refinement in Z and Object-Z. FACIT. Springer, Heidelberg (2001)

    Google Scholar 

  10. Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. PHI (1992)

    Google Scholar 

  11. Cooper, D., Stepney, S., Woodcock, J.: Derivation of Z Refinement Proof Rules. Technical Report YCS-2002-347, University of York (2002)

    Google Scholar 

  12. Groves, L.: Practical Data Refinement for the Z Schema Calculus. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 393–413. Springer, Heidelberg (2005)

    Google Scholar 

  13. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. C.U.P (1996)

    Google Scholar 

  14. Lano, K., Haughton, H.: Specification in B. Imperial College Press (1996)

    Google Scholar 

  15. Habrias, H.: Specification Formelle avec B. Hermes Sciences Publications (2001)

    Google Scholar 

  16. Schneider, S.: The B-Method. Palgrave (2001)

    Google Scholar 

  17. Abrial, J.R.: Event-B (to be published)

    Google Scholar 

  18. Rodin. European Project Rodin (Rigorous Open Development for Complex Systems) IST-511599, http://rodin.cs.ncl.ac.uk/

  19. The Rodin Platform, http://sourceforge.net/projects/rodin-b-sharp/

  20. Schellhorn, G.: Verification of ASM Refinements Using Generalised Forward Simulation. J.UCS 7(11), 952–979 (2001)

    MathSciNet  Google Scholar 

  21. Börger, E.: The ASM Rrefinement Method. Form. Asp. Comp. 15, 237–257 (2003)

    Article  MATH  Google Scholar 

  22. Banach, R.: On Regularity in Software Design. Sci. Comp. Prog. 24, 221–248 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  23. Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)

    Google Scholar 

  24. Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: Météor: A Successful Application of B in a Large Project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  25. Owe, O.: Partial Logics Reconsidered: A Conservative Approach. F.A.C.S. 3, 1–16 (1993)

    Google Scholar 

  26. The Eclipse Project, http://www.eclipse.org/

  27. Fraser, S., Banach, R.: Configurable Proof Obligations in the Frog Toolkit. In: Proc. IEEE SEFM 2007, pp. 361–370. IEEE Computer Society Press, Los Alamitos (2007)

    Google Scholar 

  28. Fraser, S.: Mechanized Support for Retrenchment. PhD thesis, School of Computer Science, University of Manchester (2008)

    Google Scholar 

  29. Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Engineering and Theoretical Underpinnings of Retrenchment. Sci. Comp. Prog. 67, 301–329 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  30. The Isabelle Theorem prover, http://www.cl.cam.ac.uk/research/hvg/Isabelle/

  31. The Karlsruhe Interactive Verifier, http://i11www.iti.uni-karlsruhe.de/~kiv/KIV-KA.html

  32. KIV: KIV Verifications on the Web, http://www.informatik.uni-augsburg.de/swt/projects/

  33. Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 16–31. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Mondex KIV: Web presentation of the Mondex case study in KIV, http://www.informatik.uni-augsburg.de/swt/projects/mondex.html

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, M13 9PL, UK

    Richard Banach

Authors
  1. Richard Banach
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Egon Börger Michael Butler Jonathan P. Bowen Paul Boca

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Banach, R. (2008). Model Based Refinement and the Tools of Tomorrow. 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_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87603-8_5

  • 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)

Publish with us

Policies and ethics

Search

Navigation