Geraint Jones: The Queen's Award for Technological Achievement 1992 Oxford and I ---<>--- ``Her Majesty the Queen has been graciously pleased to approve the Prime Minister's recommendation that The Queen's Award for Technological Achievement should be conferred this year upon Oxford University Computing Laboratory.'' ---<>--- For those of you who have never heard of the Queen: the one I mean is the little woman that the Americans hid behind a lectern last time she was there, and who appears on stamps and money both in Britain and various other places that used to be painted pink on real maps of the world. It is her birthday again today, bless her. For those of you who have never heard of Queen's Awards: where were you two years ago when Oxford University Computing Laboratory last felt inordinately pleased with itself for having won a Queen's Award? It is an institutional equivalent of an OBE or a knighthood or something like that. For twenty-seven years, each year on the Queen's birthday awards have been announced for Export and for Technological Achievement. These give the recipient the right to display an emblem* and generally feel pleased with itself. and for Technological Achievement. These give the recipient the right to display an emblem* and generally feel pleased with itself. * `The crown and cogwheels' --- if you are in Oxford you will see a huge one teetering on the edge of the Laboratory's mudbath and temporary amphitheatre (described optimistically as a `major extension') and if you are not in Oxford you will no doubt soon see a second one appear on the Laboratory's letterheads. This award is made jointly to OUCL and IBM, for their collaboration in the use of formal methods -- `notations, theories, and processes', and specifically the use of the Z notation -- in the production of transaction processing software -- and specifically the Customer Information Control System (CICS) products in IBM's Enterprise Systems Architecture (ESA) environment. ---<>--- For a decade now, Oxford University Computing Laboratory and IBM UK Labora- tories, Hursley Park, have been collaborating closely on the development of modern software engineering techniques, and their use in industrial practice. OUCL has been offering advice on mathematical techniques relevant to IBM's work, and helping IBM to apply them. Central to this collaboration has been the use of Z: in essence elementary set theory and logic, engineered into a notation suitable for the specification, development and documentation of software systems; together with techniques and styles of use. The aim of applying this `ruggedised' mathematics to the development of computer programs is to reduce the costs and risks of the process of development, and to improve the quality of the product -- which itself reduces the costs of subsequent maintenance. Before the collaboration which this award recognises, the use of Z had been confined mainly to small exercises, and largely within Oxford. The collaboration began tentatively, with small experiments to see whether Z really could be used in an industrial environment. Case studies which came from these experiments have proved useful foundations for subsequent work, but the most useful outcome was a significant transfer of culture -- in both directions -- between the academics and the practitioners. It was then decided to use Z to develop the next release of a transaction processing system, CICS/ESA_V3.1, and to this end Z was integrated into IBM's existing and well-established development process. This has demonstrated processing system, CICS/ESA_V3.1, and to this end Z was integrated into IBM's existing and well-established development process. This has demonstrated that it is possible to manage a large and important software development using mathematics. Informally (and I would rather not be held to this if anyone wants to dispute it) I understand that one of the real benefits of the exercise was precise documentation for the developers of the next version of CICS of what users of existing versions might reasonably be expecting. Many measurements of the process of developing CICS/ESA_V3.1 were conducted by IBM, and they estimate that over all the other benefits of the experiment they were able to reduce their costs for the development by almost five and a half million dollars -- rather more than three million pounds sterling. Early results from customers indicate significantly fewer problems, and those that have been detected are less severe than would be expected otherwise. (See Steve King's report on experiences of the use of Z at IBM Hursley.) ---<>--- The mingling of cultures has been of substantial benefit both to Oxford and to IBM. A choice example is the resolution of a problem in describing the correctness of a data-refinement step. One of the CICS designers knew that the step was valid, but the theory of refinements was unable formally to justify it. Research into this problem gave rise both to a new theory (complete in the technical sense), and a (complete in the usual sense) formal justification of the actual refinement. The industry in general has benefited from IBM's support and encouragement for the standardisation of Z. The syntax and semantics in the standard are both closely based on work funded by IBM. Throughout the project there has been a policy of open publication, both of techniques and results, to an extent which has been unusual for IBM in projects of this kind. This openness has contributed not a little to the acceptance of formal methods in other parts of the industry (and in particular to the spread of Z). It is pleasing to be able acknowledge that IBM's contribution to this work included not only their own staff's time and financial support of staff at the laboratory, but also the bravery to commit to an experiment involving a substantial product development, and the persistence to see it through. There has been a good understanding at all levels of management in IBM of what formal methods can and cannot do: this has enabled them to direct the Laboratory's research at the most pressing problems. Education has been an important part in this work: OUCL has taught these methods both to the students on its MSc course in Computing, and on external courses to commercial organisations, including of course IBM. (Courses in Z and its use are now also given by other organisations.) IBM has developed its own courses in consulation with Oxford, and this transfer of technology is as much a benefit of the collaboration as are the others, and is a welcome indicator that IBM had accepted that it had a stake in the methods. ---<>--- To quote (almost) verbatim from what I said here about a collaboration between the Laboratory and another company whose name began with `I', a collaboration which was similarly recognised two years ago:- `The moral of this tale is that formal methods can not only improve quality, but also the timeliness and cost of producing state-of-the-art products. [IBM], bless them, ought to have made a packet out of getting it right, being confident that they got it right, and doing so on time. The Laboratory has also benefited from the opportunity to develop its work on the underlying theory into something which it has confidence will be useful.' The project started with Ian Hayes and Ib Holm Sorensen as research officers ; today the project is led jointly by Tony Hoare and Jim Woodcock, with Steve King and Jane Sinclair as the research officers, and John Nicholls as a consultant. The list of relevant publications below gives a good guide to others involved over the years: a strength of this project has been the breadth and depth of the Z community in which it was able to flourish. Selected bibliography ~~~~~~~~~~~~~~~~~~~~~ This work has been well-documented in the scientific literature, and there is a substantial and flourishing bibliography which is maintained by the gods of comp.specification.z (send an e-mail message containing the command "help" to the address for further information). These are a few of the documents relevant to this project: S M Brien, Z Base Standard -- Version 0.5, Oxford University Computing Laboratory, ZIP/PRG/91/43, 1991. Z Base Standard -- Version 0.5, Oxford University Computing Laboratory, ZIP/PRG/91/43, 1991. B P Collins, J E Nicholls, I H Sorensen, Introducing Formal Methods: the CICS Experience with Z, Technical Report TR12.260, IBM Hursley Park, December 1987. B P Collins, C J Nix, The use of software engineering, including the Z notation, in the development of CICS, Quality Assurance. 14(2):103-110, September 1988. P H B Gardiner, P J Lupton, J C P Woodcock, A simpler semantics for Z, in Z User Workshop, Oxford 1990, Springer Workshops in Computing, 1991. I J Hayes (ed.), Specification Case Studies, Prentice Hall, 1987. P Johnson, Experience of formal development in CICS, in J McDermid (ed) The Theory and Practice of Refinement, Butterworths, 1989. S King, Z and the Refinement Calculus, PRG monograph PRG-79, Oxford University Computing Laboratory, 1990. S King, The use of Z at IBM Hursley: experience and results, Oxford University Computing Laboratory, 1991. S King, I H Sorensen, J C P Woodcock, Z: grammar and abstract and concrete syntaxes, PRG monograph PRG-68, Oxford University Computing Laboratory, 1987. P J Lupton, Promoting forward simulation, Z User Workshop, Oxford 1990, Springer Workshops in Computing, 1991. M A McMorran, J E Nicholls, Z User Manual, Technical Report TR12.274, IBM Hursley Park. J C P Woodcock, Mathematics as a management tool: proof rules for promotion, in B A Kitchenham (ed) Software Engineering for large software systems, Elsevier, 1990. J C P Woodcock, Calculating properties of Z specifications, ACM Software Engineering Notes, 14(5):43-54, 1989. J B Wordsworth, Formal methods in the development of CICS, BCS Computer Bulletin, December 1987. J B Wordsworth, Program construction from a formal specification, The Theory and Practice of Refinement, Butterworths, 1989. ---<>--- --comp.software-eng F Deutschmann: Z Specification Language -- Does anyone use it? 1 Oct 92 00:41 I have been reading a great deal about Z, the formal specification language recently, and I was curious if anyone out here on the net has experience with or actively uses Z (or another formal specification language/system) in real and/or academic projects. I'm not real interested in Z theory, but rather I am interested in real-world, real-project experience with Z. What sort of projects do people actually specify in Z? Do they tend to be multi-gazillion dollar century-long projects, or do-it-in-a-week projects, or everything in between? How do programmers, analysts, end users, and everyone in between react to Z? Any thoughts? (I'm not real interested in starting a formal spec vs. prototype debate/brawl/war, but, on the other hand, that may actually be an interesting thread to take up...) -- -frank(fhd@panix.com) -- ------ IBM(UK) has done some work with Z, namely the specification of the interface to CICS [Houston90], and I have heard of other industrial uses of Z (including BP and Praxis), although industrials tend to be a bit cagey about releasing reports into the public domain, so its unlikely you'll see anything describing how useful Z is from a practical viewpoint. From the academic viewpoint, you could check out the proceedings of the conferences organised by the Z User Group (published by Springer-Verlag), and also the VDM conferences (also published by Springer-Verlag). [Houston90] Houston, I. and Wordsworth, J., A Z specification of part of the CICS file control API, Doc. No. TR12.272 IBM(UK) Labs Ltd. Andy Coombes Phone: (0904) 433385 Department of Computer Fax: (0904) 432767 Science, Janet: andyc@uk.ac.york.minster University of York, UUCP: ...!mcsun!uknet!minster!andyc Heslington, ARPA: andyc%minster.york.ac.uk@nsfnet-relay.ac.uk YORK ------------- Karen Fabrizius: >>>Z Specification Language -- Does anyone use it? 1992 20:49 nrr@sei.cmu.edu (Neal Reizer) writes: > Two other articles related to the CICS work that are top-level summaries are: > > "CICS project report, Experiences and Results from the use of Z in IBM", > Iain Houston and Steve King. > > "The use of software engineering, including the Z notation, in the > development of CICS", C.J. Nix and B.P. Collins. > > I'm sorry that I don't have the complete reference, but perhaps an author > search may get you in the right direction. > > Neal Reizer > > > Neal Reizer nrr@sei.cmu.edu > Research Assistant (412) 268-2854 > Software Engineering Institute I just "happen" to have these references: Iain Houston and Steve King. "Experiences and results from the use of Z in IBM" In VDM '91: Formal Software Development Methods, number 551 in Lecture Notes in Computer Science, pp. 588-595. Springer-Verlag, October 1991. and C.J. Nix and B.P. Collins. "The use of software engineering, including the Z notation, in the development of CICS." Quality Assurance, 14(3):103-110, September 1988 Karen Fabrizius kcf@cs.cmu.edu ----------------------- Lucy Chubb: >Z Specification Language -- Does anyone use it? 2 Oct 92 04:44 From article <1992Oct1.004147.1757@panix.com>, by fhd@panix.com (Frank Deutschma nn): [...] I used Z to do the functional specification of a project I led last year. I use Z all the time in my (part time) Phd, but that was the first time I had used it at work. [...] The project was something like a man-year of effort over three months of real time. It involved communications and databases. The Z spec ended up being an appendix to the functional design document. There was a mixed reaction from others, but I was designing the thing and I find that specs end up having too many holes in them unless I use some form of formal specification. In other words, I needed to do it to help me understand the problem and design a solution. I'm most familiar with Z, so Z was what I used. Lucy Chubb. Softway Pty Ltd, Phone: +61 2 698 2322; P.O. Box 305, Fax: +61 2 699 9174; Strawberry Hills, Email: lucyc@softway.oz.au NSW 2012, AUSTRALIA ---------------------------- 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) [...] 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. --------------------------- Jonathan Bowen: >Users of Z formal specification 6 Oct 92 12:45 In article <1992Oct2.200647.19771@panix.com> fhd@panix.com (Frank Deutschmann) writes: >So, once again, I ask my question: Does anybody use Z? A survey paper that may be of interest is: R. Barden, S. Stepney and D. Cooper, The use of Z, In J.E. Nicholls, Z User Workshop, York 1991 Springer-Verlag, Workshops in Computing, 1992. To appear. This surveys a number of Z users in the UK, including some statistics and individual case histories. This should be out very soon, hopefully. -- -- Jonathan Bowen, Oxford University Computing Laboratory. --------------------------------------------------------------- 21 Apr 92 12:14 Jonathan Bowen: >Greek letters in schema names and FUZZ In article <1992Apr13.213807.17171@beaver.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes: >Does anyone know how to get FUZZ to accept schema names that have >capital Greek letters in them? To get fuzz to accept *any* names you wish, use a LaTeX macro definition for the name. E.g., for your example: \def\SFrameT{S\Phi T} \begin{zed} \SFrameT \defs SFrameT \end{zed} -- Jonathan Bowen, Oxford University Computing Laboratory. 21 Apr 92 14:09 Stephen Gilmore: >>Greek letters in schema names and FUZZ In article <3332@inca.comlab.ox.ac.uk>, bowen@prg.ox.ac.uk (Jonathan Bowen) writ es: > > To get fuzz to accept *any* names you wish, use a LaTeX macro > definition for the name. E.g., for your example: > > \def\SFrameT{S\Phi T} > > \begin{zed} > \SFrameT \defs SFrameT > \end{zed} > Using such a definition also allows an indexing command to be inserted: \newcommand{\SFrameT}{S{\Phi}T\index{Schema $S{\Phi}T$}} The "makeindex" program for LaTeX can then be used to generate a page number index which lists every reference to the schema \SFrameT. Stephen Gilmore Laboratory for Foundations of JANET: stg@dcs.ed.ac.uk Computer Science UUCP: ..!mcsun!uknet!dcs!stg Department of Computer Science ARPA: stg%dcs.ed.ac.uk@nsfnet-relay.ac.uk The James Clerk Maxwell Building The King's Buildings University of Edinburgh Tel: (+44) 031-650-5189 Edinburgh EH9 3JZ, UK. Fax: (+44) 031-667-7209 anyone know how to get FUZZ to accept schema names that have capital Gree k | letters in them? | | ... | | Am I missing something that is obvious to LaTeX adepts, or are such schema | names just not permitted with FUZZ? | | Also, is it possible to have hyphens in schema names? For example, S-Frame-T. | LaTeX/FUZZ sees these as minus signs. I know about underscores, but hyphens | are used in the case studies book, and some people prefer them. Sooner or later this question arises to everyone working with FUZZ, so I'll answer it to all of you, not just Jon: The problem is that FUZZ expects a single identifier at certain places and you want those identifiers look somehow unfamiliar. All you have to do is to define an identifier via `\newcommand' which can look as funny as you like it. Some examples: \newcommand{\PhiState}{\Phi State} % framing schema \newcommand{\SchemaName}{\hbox{\it Schema-Name}} % hyphenation \newcommand{\LambdaNat}{\Lambda_\nat} % \nat as index -- +---------------------------------------+--------------------------------+ | Martin Carstensen | cash@infko.uni-koblenz.de | | Universitaet Koblenz | | | Fachbereich Informatik | Voice: +49 261 9119-423 | | Rheinau 3-4, D-5400 Koblenz, Germany | Fax: +49 261 9119-499 | +---------------------------------------+--------------------------------+ 22 Apr 92 18:35 Peter Johnson: Z Compilers Does anybody know if it is possible to compile Z like a conventional programming language? I've written something which uses the macro facilities of C but it is quite crude and doesn't handle sets too well. Has anybody tried this? -- Peter Johnson 24 Apr 92 07:11 Huis in't Veld: Specifying and Designing in Z Hello, I'm interested in the use of Z to specify and design protocols and datacommunication architectures. Can anyone out there provide me with pointers t o this. Thanks ------------------------------------------------------------------- | Robert Huis in 't Veld tel. +31 53 893678 | | University of Twente fax. +31 53 333815 | | Dept. of Computing Science | | Tele-Informatics & Open Systems Group | | P.O. Box 217 NL-7500 AE Enschede The Netherlands | ------------------------------------------------------------------- -- ------------------------------------------------------------------- | Robert Huis in 't Veld tel. +31 53 893678 | | University of Twente fax. +31 53 333815 | | Dept. of Computing Science | | Tele-Informatics & Open Systems Group | | P.O. Box 217 NL-7500 AE Enschede The Netherlands | ------------------------------------------------------------------- 24 Apr 92 09:48 zforum-request: >Postscript Z Fonts cmann@kurango.cit.gu.edu.au (Craig Mann) writes: | |hs0bth@orac.sundp.ac.uk (B.THOMPSON) writes: | |>I have tried to send copies of both versions of the font to everyone who |>has asked. However, our local NRS table hasn't heard of some people's |>machines. |>Jonathan Bowen is adding the fonts to the archive at the PRG, so it might be |>better to get them from there. | | |Where is PRG? Could you please include the full address. I have installed the PostScript Z font files that Brian Thompson sent me under the Z category on the PRG archive server as follows: zfont.readme Brief overview of the following files zfont.type1 Type 1 PostScript font for Z symbols zfont.type3 Type 3 PostScript font for Z symbols zfont.riscos Original "RISCOS" font from which the above are derived Send an e-mail message including the command: "send z zfont.readme zfont.type1" (for example) to to obtain the files you require. Send a command of "help" for more information on using the archive server. Please direct enquiries to Brian Thompson if you have further queries. These files contain all the information that *I* have; I haven't tried using them myself. -- Jonathan Bowen, PRG archive maintainer. 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) EUROKOM: Malcolm_Harper@eurokom.ie (Attn J.P.Bowen) 26 Apr 92 17:58 s shirish: Z Macro's in Latex wanted. Hi Everyone, I would like to know if there are any Z style macro's available and how one could get them? Please respond directly via Email to the address below. Thanx in advance. shirish -- ///////////////////////////////////////////////////////////////////////// / shirish seetharam | / / Colorado State Univ. | / / shirish@mozart.cs.colostate.edu | / ///////////////////////////////////////////////////////////////////////// 20 Apr 92 12:01 Cliff B Jones: Formal Methods Europe --------------------------------------------------------------------- <<< CALL FOR PAPERS >>><<< CALL FOR PAPERS >>><<< CALL FOR PAPERS >>> <<< CALL FOR PAPERS >>><<< CALL FOR PAPERS >>><<< CALL FOR PAPERS >>> <<< CALL FOR PAPERS >>><<< CALL FOR PAPERS >>><<< CALL FOR PAPERS >>> FME '93 SYMPOSIUM "INDUSTRIAL STRENGTH FORMAL METHODS" Sponsored by the Commission of the European Communities (CEC) Organised by Formal Methods Europe The first FME Symposium will be held at Odense Technical College in Denmark, during the week of 19 to 23 April, 1993. It is being organised by Formal Methods Europe, as the successor to the last four VDM symposia, to promote the interests of users, researchers and developers of precise mathematical methods in program development. The last few years have borne witness to the remarkable diversity of formal methods, with applications to sequential and concurrent The last few years have borne witness to the remarkable diversity of formal methods, with applications to sequential and concurrent software, to real-time and reactive systems, and to hardware design. In that time, many theoretical problems have been tackled and solved, and many continue to be worked upon. Yet it is by the suitability of their industrial application and the extent of their usage that formal methods will ultimately be judged. This symposium will focus on the application of industrial-strength formal methods. We encourage all papers to address the difficulties of scaling their techniques up to industrial-sized problems, and of their suitability in the work-place. Papers should discuss techniques that are formal (that is, they have a mathematical basis), and that are industrially applicable. Papers tackling theoretical issues are much encouraged, providing that they contain a justification of the practical advantages that follow. Full-length research papers, industrial reports, proposals for tutorials and tool demonstrations are solicited, particularly in the following areas: * Practical use * Case studies * Tools * Linking formal and informal methods * Comparisons of formal methods * Proof * Concurrency * Real-time and reactive systems * Refinement techniques * Object orientation * Secure systems * Safety-critical systems * The development process * Education and technology transfer 1 October 1992 ============== Submissions: - Full, original research papers (6 copies, 12pt, single spaced, maximum 20pp) - Industrial usage reports (6 copies, 12pt, single spaced, maximum 10pp) - Proposals for tutorials (half day, maximum 50pp of notes for participants) - Proposals for tool demonstrations (with hardware and software requirements) Proposals for tools demonstrations should be send to the organising chairman, while all other proposals should be send to the programme chairman. Industrial usage reports do not need to conform to usual standards for academic papers. 1 December 1992 =============== Notification of acceptance 1 February 1993 =============== Camera-ready copy due for publishers Programme Chairman Organising Chairman Jim C.P. Woodcock, Peter Gorm Larsen, Oxford University The Institute of Applied Computing Laboratory, Computer Science (IFAD), Programming Research Group Forskerparken 10, 11 Keble Road, DK-5230 Odense M Oxford OX1 3QD, UK Denmark tel: +44 865 272576 tel: +45 65 93 23 00 fax: +44 865 273839 fax: +45 65 93 29 99 email: jimw@prg.ox.ac.uk email: peter@ifad.dk Executive Programme Committee J.-R. Abrial (F) Tim Denvir (GB) Eugene Durr (NL) Ian Hayes (AUS) Steve King (GB) Hans Langmaack (D) Micheal Mac an Airchinnigh (IRL) Kees Middelburg (NL) Soren Prehn (DK) Hans Toetenel (NL) 20 Apr 92 23:01