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 RetrenchmentAtomicity 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.