home > publications > Formal methods and Z

in preparation

• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney.
  Retrenchment and Promotion in Z. (in preparation)

2013

journal papers

• Richard Banach, Czeslaw Jeske, Anthony Hall, Susan Stepney.
  Atomicity Failure and the Retrenchment Atomicity Pattern.
  Formal Aspects of Computing 25(3):439-464, 2013.

2008

journal papers

• Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, Jeremy L. Jacob.
  The certification of the Mondex electronic purse to ITSEC Level E6.
  Formal Aspects of Computing 20(1):5-19, 2008

2007

journal papers

• Nuno Amálio, Fiona Polack, Susan Stepney.
  Frameworks based on templates for rigorous model-driven development.
  Doctoral Symposium, IFM 2005. ENTCS 191:3-23. Elsevier, 2007

• Richard Banach, Czeslaw Jeske, Michael Poppleton, Susan Stepney.
  Retrenching the Purse : the balance enquiry quandary, and generalised and (1,1) forward refinements.
  Fundamenta Informaticae 77:29-69, 2007

• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney.
  Engineering and Theoretical Underpinnings of Retrenchment.
  Science of Computer Programming, 67(2-3):301-329, July 2007

refereed workshop and conference papers

• Richard Banach, Czeslaw Jeske, Anthony Hall, Susan Stepney.
  Retrenchment and the Atomicity Pattern.
  SEFM 07, London, UK, September 2007. IEEE Press, 2007

other

• Tuan Anh Nguyen, Fiona Polack, Susan Stepney, Ian Toyn.
  Practical use of real numbers in Z.
  Z User Meeting 2007, in conjunction with ICECCS 2007, Waikato, New Zealand, 11-14 July 2007

2006

book chapters

• Nuno Amálio, Fiona Polack, Susan Stepney.
  UML + Z: Augmenting UML with Z.
  In Marc Frappier, Henri Habrias, eds. Software Specification Methods : an Overview Using a Case Study, new edn, Hermes Science Publishing, 2006

refereed workshop and conference papers

• Nuno Amálio, Susan Stepney, Fiona Polack.
  A Formal Template Language enabling Meta-Proof.
  FM'06, McMaster University, Canada, August 2006. LNCS 4085:252-267, Springer, 2006

• Richard Banach, Czeslaw Jeske, Michael Poppleton, Susan Stepney.
  Retrenching the Purse: hashing injective CLEAR codes, and security properties.
  ISoLA 2006, Cyprus, November 2006. IEEE, 2006

• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney.
  Retrenching the Purse : finite exception logs, and validating the small.
  30th Annual IEEE/NASA Software Engineering Workshop, Columbia, MD, USA, pp234-245, April 2006

2005

refereed workshop and conference papers

• Nuno Amálio, Fiona Polack, Susan Stepney.
  An OO structuring for Z based on Views.
  ZB2005, Guildford, UK, April 2005. LNCS 3455:262-278, Springer, 2005.

• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney.
  Retrenching the Purse : finite sequence numbers and the Tower Pattern.
  FM 2005, Newcastle, UK, July 2005. LNCS 3582:382-398, Springer 2005

• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney.
  Retrenchment and the Mondex Electronic Purse (extended abstract).
  Proc. ASM'05, Paris, France, March 2005

• Jemima Rossmorris, Susan Stepney.
  Requirements as Conjectures: intuitive DVD menu navigation.
  ZB2005, Guildford, UK, April 2005. LNCS 3455:172-186, Springer, 2005.

technical reports

• Susan Stepney, Fiona Polack, Ian Toyn.
  Diagram Patterns and Meta-patterns to support formal modelling.
  Technical Report YCS-2005-394, University of York. October 2005

2004

refereed workshop and conference papers

• Nuno Amálio, Susan Stepney, and Fiona Polack
  Formal Proof from UML Models.
  ICFEM 2004, Seattle, USA. LNCS 3308:418-433, Springer, 2004

• Richard Banach, Czeslaw Jeske, Simon Fraser, Richard Cross, Mike Poppleton, Susan Stepney, Steve King.
  Approaching the Formal Design and Development of Complex Systems: the Retrenchment Position.
  Workshop on Software and Complex Systems, 9th IEEE Intl. Conf. on Engineering of Complex Computer Systems, Florence, Italy, April 2004

technical reports

• Samuel H Valentine, Susan Stepney, Ian Toyn.
  A Z Patterns Catalogue II: definitions and laws, v0.1.
  Technical Report YCS-2004-383, University of York. October 2004

2003

refereed workshop and conference papers

• Nuno Amálio, Susan Stepney, Fiona Polack.
  Modular UML Semantics: Interpretations in Z based on Templates and Generics.
  FACS'03 Workshop on Formal Aspects of Component Software, Pisa. UNU/IIST Technical Report 284. 2003

• Susan Stepney, Fiona Polack, Ian Toyn.
  An Outline Pattern Language for Z.
  ZB2003, Turku, Finland. LNCS 2651:2-19, Springer, 2003.

• Susan Stepney, Fiona Polack, Ian Toyn.
  Patterns to Guide Practical Refactoring.
  ZB2003, Turku, Finland. LNCS 2651:20-39. Springer, 2003.

technical reports

• Susan Stepney, Ian T. Nabney.
  The DeCCo Project Papers.
  Technical Report YCS-2003-358--363, University of York. June 2003.

• Susan Stepney, Fiona Polack, Ian Toyn.
  A Z Patterns Catalogue I: specification and refactorings, v0.1.
  Technical Report YCS-2003-349, University of York. January 2003.

2002

refereed workshop and conference papers

• Susan Stepney, Fiona Polack, Ian Toyn.
  Refactoring in Maintenance and Development of Z Specifications and Proofs.
  REFINE 2002, Copenhagen. ENTCS 70(3):396-415. Elsevier, 2002

• Ian Toyn, Susan Stepney.
  Characters + Mark-up = Z Lexis.
  ZB2002, Grenoble, France. LNCS 2272:100-119, Springer, 2002.

technical reports

• David Cooper, Susan Stepney, Jim Woodcock.
  Derivation of Z Refinement Proof Rules.
  Technical Report YCS-2002-347, University of York. December 2002.

2001

other

• Susan Stepney.
  New Horizons in Formal Methods.
  The Computer Bulletin, pp 24-26. BCS, January 2001.

2000

refereed workshop and conference papers

• David Cooper, Susan Stepney.
  Segregation with Communication.
  ZB2000, York, UK. LNCS 1878:451-470, Springer, 2000.

• Susan Stepney, David Cooper.
  Formal Methods for Industrial Products.
  ZB2000, York, UK. LNCS 1878:374-393, Springer, 2000.

• Ian Toyn, Samuel H Valentine, Susan Stepney, Steve King.
  Typechecking Z.
  ZB2000, York, UK. LNCS 1878:264-285, Springer, 2000.

• Samuel H Valentine, Ian Toyn, Susan Stepney, Steve King.
  Type-constrained Generics for Z.
  ZB2000, York, UK. LNCS 1878:250-263, Springer, 2000.

technical reports

• Susan Stepney, David Cooper, Jim Woodcock.
  An Electronic Purse: Specification, Refinement, and Proof.
  Technical Monograph PRG-126, Oxford University Computing Laboratory. July 2000.

1999

refereed workshop and conference papers

• Fiona Polack, Susan Stepney.
  Systems Development using Z Generics.
  FM '99, Toulouse, France. LNCS 1709:1048-1067, Springer, 1999.

1998

refereed workshop and conference papers

• Susan Stepney.
  Incremental Development of a High Integrity Compiler: experience from an industrial development.
  Third IEEE High-Assurance Systems Engineering Symposium (HASE'98), Washington DC, USA. 1998.

• Susan Stepney.
  A Tale of Two Proofs.
  BCS-FACS Third Northern Formal Methods Workshop, Ilkley, UK. Electronic Workshops in Computing, 1998.

• Susan Stepney, David Cooper, Jim Woodcock.
  More powerful Z data refinement: Pushing the State of the Art in industrial refinement.
  ZUM '98, Berlin, Germany. LNCS 1493:284-307, Springer, 1998.

1997

refereed workshop and conference papers

• David W. J. Stringer-Calvert, Susan Stepney, Ian Wand.
  Using PVS to prove a Z refinement: a case study.
  FME '97, Graz, Austria. LNCS 1313. Springer, 1997.

1995

refereed workshop and conference papers

• Susan Stepney.
  Testing as Abstraction.
  ZUM'95, Limerick, Ireland. LNCS 967:137-151, Springer, 1995.

other

• Jonathan Bowen, Susan Stepney, Rosalind Barden.
  Annotated Z Bibliography.
  Information and Software Technology, 37(5-6):317-332, 1995.

1994

books / proceedings

• Rosalind Barden, Susan Stepney, David Cooper.
  Z in Practice.
  BCS Practitioner Series. Prentice-Hall, 1994.

1993

books / proceedings

• Susan Stepney.
  High Integrity Compilation: a case study.
  Prentice-Hall, 1993.

refereed workshop and conference papers

• Rosalind Barden, Susan Stepney.
  Support for using Z.
  Proceedings of the 7th Z User Meeting, London, 1992, Workshops in Computing, pp 255-280. Springer, 1993.

other

• Susan Stepney, Rosalind Barden.
  Annotated Z Bibliography.
  EATCS Bulletin, 50:280-313. June 1993.

1992

books / proceedings

• Susan Stepney, Rosalind Barden, David Cooper, editors.
  Object Orientation in Z.
  Workshops in Computing. Springer, 1992.

journal papers

• Susan Stepney, Rosalind Barden, David Cooper.
  A Survey of Object Orientation in Z.
  Software Engineering Journal, 7(2):150-160, March 1992.

refereed workshop and conference papers

• Rosalind Barden, Susan Stepney, David Cooper.
  The Use of Z.
  Proceedings of the 6th Z User Meeting, York, UK, 1991, pp 99-124. Workshops in Computing, Springer, 1992.

other

• Susan Stepney.
  Summary of the BCS-FACS Christmas Meeting on Domain Theory.
  Jawed Siddiqi, editor, BCS-FACS FACTS Newsletter, Series II, 3(1):4-7. May 1992.

1991

journal papers

• Susan Stepney, Dave Whitley, David Cooper, Colin Grant.
  A Demonstrably Correct Compiler.
  Formal Aspects of Computing, 3:58-101. BCS, 1991.

1987

journal papers

• Susan Stepney, Stephen P. Lord.
  Formal Specification of an Access Control System.
  Software-Practice and Experience, 17(9):575-593, 1987.