🚀 go-pugleaf

From:  Martin Weigele <weigele@rz.informatik.uni-hamburg.dbp.de>
To: mod-ki@unido.informatik.uni-dortmund.de
Date: 30 Apr 90 18:15 +0100
Subject: Ihrer Majestaet Preis fuer Formale Spezifikation
Keywords: Spezifikation, Verifikation, Parallelverarbeitung, Transputer

mod-ki message 0453
************************************************************************
Fuer alle, die bisher vergeblich auf reale Beispiele fuer  erfolgreichen
Einsatz von Methoden der Programm-Spezifikation gewartet haben, sei  der
nachfolgende Artikel von Geraint Jones mit dessen freundlicher Erlaubnis
wiedergegeben (c) Geraint Jones, Oxford, 1990.  Mir  sei  die  Anmerkung
erlaubt, dass dieser  Erfolg  wesentlich  auf  das  Prinzip  "clear  and
simple" zurueckzufuehren sein  duerfte,  etwas,  was  ich  in  deutschen
Landen schon oft vergeblich gesucht habe...

Martin Weigele, FB Informatik, Univ. Hamburg

==================
From: Geraint.Jones@uk.ac.oxford.prg (Geraint Jones)
Newsgroups: ox.general
Subject: The Queen's Award for Technological Achievement 1990, INMOS and
Oxford
Date: 20 Apr 90 23:43:16 GMT
Lines: 121

``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.''
                                    ---<>---
 
``This award goes jointly to  Oxford University Computing Laboratory and
  INMOS Ltd,  for the development of formal methods in the specification
  and design of microprocessors.
 
``The occam programming language,  developed  by the applicants has been
  used  to  translate  the IEEE Standard 754 to cover the floating point
  arithmetic unit for the IMS T800 floating point transputer.
 
``The  use  of  formal  methods  has  enabled the development time to be
  reduced by 12 months.''
                                    ---<>---

For those of you who have  never  heard  of  Queen's  Awards,  I  should
explain that it is an institutional equivalent of an OBE or a knighthood
or something like that. For twenty-five years, awards for Export and for
Technological Achievement have been announced on  the  Queen's  birthday
(today) which give the recipient the right to display an emblem (`the
crown and cogwheels') and generally feel pleased with itself.

This is the first time that a department of the University has  achieved
the distinction of a Queen's Award, and the Computing Laboratory is  one
of only  three  university  research  groups  amongst  this  year's  175
award-winners. The great thing about this award is  that  it  recognises
the value of University research in promoting technological development.

For those of you who have not heard before of the work  being  honoured,
perhaps I could explain. The award cites the development of occam, which
is the first commercially  available  language  to  take  seriously  the
problem of programming MIMD parallel machines. Occam goes out of its way
to be clear and simple, being designed to be very little  more  than  an
implementation of Tony Hoare's CSP.  The  intellectual  leverage  gained
from  the  simplicity  and  elegance  of  the  semantics  of  occam,  is
instrumental in the success of the project.

The most tangible commercial success is the design of the floating point
arithmetic unit in the T800 transputer. The heroes  of  this  tale  (the
ones who did the work anyway) are Geoff Barrett and David Shepherd, both
of whom came to Oxford as students on the MSc in Computation,  and  both
of whom now work for INMOS Ltd in Bristol. At the time the work was done
Geoff was in Oxford doing  his  doctoral  research  in  the  Programming
Research Group, and David was designing chips for INMOS.

When the T800 transputer was designed it was decided  that  in  parallel
with an informal development, supported by  months  of  testing  against
other  FPUs,  a  team  would  set  about  a  formal  development  of   a
correct-by-design unit. In this context `correct'  means  conforming  to
the IEEE Standard 754, and a big first step was to decide  exactly  what
the specification required. The IEEE document is partly reliant  on  the
meaning of natural language requirements; Geoff Barrett's  recasting  of
the Standard into the Z specification language [1,2] is unambiguous  and
serves as the touchstone for the correctness of the T800 FPU.

The microcode of the T800 FPU was documented in a restricted  subset  of
occam. Using the occam transformation system  developed  in  Oxford [3],
David Shepherd demonstrated that this code  was  equivalent  to  a  more
naturally expressed occam program which had been shown  to  meet  the  Z
specification. The transformation system builds on the simple  semantics
of occam, as expressed by Bill Roscoe and Tony Hoare  in  [4],  allowing
essentially mechanical proof that two programs -- like the specification
of the FPU and the implementing microcode -- have the same effect.

You could hardly have made a better case for formal methods, because the
race went to the formal development method. Moreover a number of  errors
were found in the proposed implementation  that  had  not  shown  up  in
months of necessarily very limited testing. (Some of  the  discrepancies
found in testing transpired to be mistakes in  an  implementation  by  a
competitor, against which the simulation of the T800 was being compared)
Not only is it possible to be much more confident in the accuracy of the
finished FPU, but this higher  quality  implementation  was  cheaper  to
design, and completed an estimated year ahead of  what  would  otherwise
have been achievable.

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. INMOS, 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.

There is a very readable  non-technical  summary  of  this  work  in  an
article in New Scientist last year [5].

The other people in Oxford working on the occam  transformation  project
(of  which  the  T800  FPU  work  was  a  part)  who   implemented   the
transformation system were Michael Goldsmith  and  Tony Cox.  With  Bill
Roscoe and others they are involved in a company called  Formal Systems,
selling just this kind of expertise,  which  works  out  of  offices  in
Oxford and in Auburn, Alabama; and Bill is a lecturer at the  University
of Oxford.

                            References
                            ~~~~~~~~~~
1. Geoff Barrett,
        Formal Methods applied to a Floating Point Number System,
        Programming Research Group technical monograph PRG-58,
        Oxford University Computing Laboratory, January 1987.
 
2. Geoff Barrett,
        Formal Methods applied to a Floating point Number System,
        in IEEE Trans Soft Eng, May 1988. pp 611-621.
 
3. Michael Goldsmith,
        The Oxford occam Transformation system (documentation),
        Programming Research Group,
        Oxford University Computing Laboratory, 1988.
 
4. A. W. Roscoe and C. A. R. Hoare,
        The Laws of occam Programming,
        Programming Research Group technical monograph PRG-53,
        Oxford University Computing Laboratory, February 1986.
 
5. David Shepherd and Greg Wilson,
        Making Chips that Work,
        New Scientist, No 1664, 13 May 1989. pp 61-64.
************************************************************************