From: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen)
Newsgroups: comp.software-eng
Subject: Re: Z Specification Language -- Does anyone use it?
Date: 2 Oct 92 09:09:34 GMT
Organization: Programming Research Group, Oxford University, UK
X-Mailer: mail-news 2.0.3

In article <1992Oct1.205501.9359@sei.cmu.edu>:
|
|In article <717933199.4476@minster.york.ac.uk>, andyc@minster.york.ac.uk writes:
|
|I'm sorry that I don't have the complete reference, but perhaps an author
|search may get you in the right direction.
|

Unfortunately many real uses of Z remain unpublished because of
commercial and security reasons. However, below are some published
references to real uses of Z mostly from the Z bibliography (for access
details, see the monthly FAQ message in the newsgroup
comp.specification.z, where more info and discussion on Z can be
found).

Both the first two example of the use of formal methods have won
Queen's Awards for Technological Achievement in the UK, in 1990 and
1992 respecively. This probably doesn't mean much to people outside the
UK, but are national awards given to a few dozen organizations each
year for examples of technology where financial and other benefits can
be demonstrated. Inmos claim to have saved 12 months development time,
and IBM claim a 9% overall cost saving (millions of $s for them) as a
result.

I would be very interested in hearing about other published and
unpublished examples of the real use of Z, both successful and
unsuccessful.

--
Jonathan Bowen
Oxford University Computing Laboratory, Programming Research Group
11 Keble Road, Oxford OX1 3QD, England.
Tel:     +44-865-272574 (direct) or 273838 (general)
FAX:     +44-865-272582 (direct) or 273839 (general)
Email:   Jonathan.Bowen@comlab.ox.ac.uk (direct)
         comlab@comlab.ox.ac.uk (general)


----------------------- Real-use Z references -----------------------

IBM CICS transaction processing system development:

@article{Z:Nix88,
  author = {C.J. Nix and B.P. Collins},
  title = {The use of Software Engineering, including the {Z} Notation,
    in the Development of {CICS}},
  journal = {Quality Assurance},
  volume = {14},
  number = {3},
  pages = {103-110},
  month = {September},
  year = {1988}
}

@inproceedings{Z:Phil90,
  author = {M. Phillips},
  title = {{CICS/ESA} 3.1 Experiences},
  booktitle = {{Z} User Workshop, {Oxford} 1989},
  editor = {John E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  location = {Rewley House, Oxford, UK, 15 December 1989},
  pages = {179-185},
  year = {1990}
}

@inproceedings{Z:Hous91,
  author = {Iain S.C. Houston and Steve King},
  editor = {S. Prehn and W.J. Toetenel},
  title = {{CICS} Project Report: Experiences and Results
    from the Use of {Z} in {IBM}},
  booktitle = {{VDM'91}: Formal Software Development Methods},
  publisher = {Springer-Verlag},
  series = lncs,
  volume = {551},
  pages = {588-596},
  year = {1991}
}


Inmos transputer FPU microcode development:

@article{Z:Barr89,
  author = {Geoff Barrett},
  title = {Formal Methods Applied to a Floating-Point Number System},
  journal = {IEEE Transactions on Software Engineering},
  volume = {15},
  number = {5},
  pages = {611-621},
  month = {May},
  year = {1989},
  annote = {
    This paper presents a formalisation of the IEEE standard for binary
    floating-point arithmetic in Z. The formal specification is refined
    into four components. The procedures presented form the basis for
    the floating-point unit of the Inmos IMS T800 transputer.
    This work resulted in a joint Queen's Award for technological
    achievement for Inmos Ltd and the Oxford University Computing
    Laboratory in 1990. It was estimated that the approach saved a
    year in development time compared to traditional methods.}
}

@article{Z:Shep89,
  author = {David E. Shepherd and Greg Wilson},
  title = {Making Chips that Work},
  journal = {New Scientist},
  volume = {1664},
  pages = {61-64},
  month = {May},
  year = {1989},
  annote = {A general article containing information on the
    formal development of the T800 floating-point unit for the
    transputer including the use of Z.}
}

@incollection{Z:May90,
  author = {David May},
  editor = {C.A.R. Hoare},
  title = {Use of Formal Methods by a Silicon Manufacturer},
  booktitle = {Developments in Concurrency and Communication},
  publisher = {Addison-Wesley Publishing Company},
  series = {University of Texas at Austin Year of Programming Series},
  chapter = {4},
  pages = {107-129},
  year = {1990}
}

@article{Z:Shep90,
  author = {David E. Shepherd},
  editor = {Hussein Zedan},
  title = {Verified Microcode Design},
  journal = {Microprocessors and Microsystems},
  month = {December},
  year = {1990},
  volume = {14},
  number = {10},
  pages = {623-630},
  annote = {
    This article shows how a high-level program in Occam was
    transformed to a low level implementation that matched the
    micromachine functions of the T800 transputer in order to verify
    its microcode.  The high-level specification is first given in Z.
    The article is part of a special issue on {\em Formal aspects of
    microprocessor design}, edited by Hussein Zedan.  See also
    \cite{Z:Bowe90d}.}
}

Just out:

D. May, G. Barrett and D. Shepherd,
Designing chips that work,
in C.A.R. Hoare and M.J.C. Gordon (eds.),
Mechanized reasoning and hardware design,
Prentice Hall International Series in Computer Science,
pp. 3--19, 1992.


Tektronix oscilloscope specification:

@inproceedings{Z:Deli89,
  author = {Norman Delisle and David Garlan},
  title = {Formally Specifying Electronic Instruments},
  booktitle = {Proc.\ Fifth International Workshop on
    Software Specification and Design},
  publisher = {IEEE Computer Society},
  month = {May},
  year = {1989},
  note = {Also published in ACM SIGSOFT Software Engineering Notes
    14(3)}
}

@article{Z:Deli90,
  author = {Norman Delisle and David Garlan},
  title = {A Formal Specification of an Oscilloscope},
  journal = {IEEE Software},
  pages = {29-36},
  month = {September},
  year = {1990},
  annote = {
    Unlike most work on the application of formal methods, this
    research uses formal methods to gain insight into system
    architecture. The context for this case study is electronic
    instrument design.}
}


I hope some of these are helpful.