School of Computing - University of Teesside - Middlesbrough (UK)

Menu of Content

B and Z

B and Z are two of the major specification and modelling notations in the Formal Methods area, and share a common lineage in the work of J-R Abrial. Conceived originally for specifying and (in the case of B) implementing sequential programs, they have proved equally useful in the conceptualisation and modelling of distributed systems.

  1. S. E. Dunne and S. Conroy. Process refinement in B. In H. Treharne, S. King, M. C. Henson, and S. Schneider, editors, ZB2005: Formal Specification and Development in Z and B, number 3455 in Lecture Notes in Computer Science, pages 45-64. Springer, 2005.
  2. S. E. Dunne. Understanding Object-Z operations as generalised substitutions. In Eerke A. Boiten, John Derrick, and Graeme Smith, editors, Integrated Formal Methods, 4th International Conference, IFM 2004, number 2999 in Lecture Notes in Computer Science, pages 328-342. Springer-Verlag, 2004.
  3. S. E. Dunne. Introducing backward refinement into B. In D. Bert, J. P. Bowen, S. King, and M. Walden, editors, ZB2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users, number 2651 in Lecture Notes in Computer Science, pages 178-196. Springer-Verlag, 2003.
  4. S. E. Dunne. A theory of generalised substitutions. In D. Bert, J. P. Bowen, M. C. Henson, and K. Robinson, editors, ZB2002: Formal Specification and Development in Z and B, number 2272 in Lecture Notes in Computer Science, pages 270-290. Springer-Verlag, 2002.
  5. J. P. Bowen, S. E. Dunne, A. J. Galloway, and S. King, editors. ZB2000: Formal Specification and Development in Z and B, number 1878 in Lecture Notes in Computer Science. Springer Verlag, 2000.
  6. S. E. Dunne. The safe machine: a new specification construct for B. In J. M. Wing, J. Woodcock, and J. Davies, editors, FM'99 - Formal Methods, number 1708 in Lecture Notes in Computer Science, pages 472-489. Springer Verlag, 1999.
  7. S. E. Dunne, W. J. Stoddart, and A. J. Galloway. Specification and refinement in general correctness. In A. Evans, D. Duke, and A. Clark, editors, Proceedings of the 3rd Northern Formal Methods Workshop. BCS Electronic Workshops in Computing, 1998. http://www.ewic.org.uk/ewic/workshop/view.cfm/NFM-98.
  8. S. E. Dunne, W. J. Stoddart, and A. J. Galloway. Hypersubstitutions: extending the generalised substitution to model semi-decidable operations. In H. Habrias, editor, The First B Conference. Universite de Nantes, 1996. ISBN 2-906082-25-2.
  9. S. E. Dunne. Formal modelling in Z: a top-down approach. In Proceedings of ACIS 95, the 6th Australian Conference on Information Systems, pages 877-892. 1995. ISBN 1-86342-464-4.
If you have difficulties accessing this website please email d.cumbor {at} tees.ac.uk.