- Go to the
City CSR Home Page. Review of:
Woodcock and Davies 'Using Z: Specification, Refinement and Proof'
Hinchey and Bowen, 'Applications of Formal Methods'
Both books in Prentice Hall International Series in
Computer Science
Review by Norman Fenton (Professor of Computing Science,
Centre for Software Reliability, City University, London)
Formal methods is the term computer
scientists use to refer to the use of mathematics in system
specification and development (although it has never been clear
to my why a special term is needed). In traditional engineering
disciplines, designers of complex systems routinely use
mathematical notations to specify and reason about the properties
of their designs. This enables them to identify problems before
expensive production costs are incurred. Yet, despite the fact
that software systems (or systems which contain software
components) are among the most complex systems ever built, it is
very rare for software designers to use any mathematics at all in
their specifications and designs. This means that there is no
possibility of reasoning formally about their proposed systems
until the program code is created. By this stage a considerable
investment of effort has already been made and crucial
specification and design faults are difficult and costly to
locate and fix. It has been claimed that this phenomenon is a
major cause of the continuing 'software crisis' of poor software
quality and late delivery. With the increasing use of software in
business-critical, and even safety critical applications, the
lack of a proper engineering approach seems reprehensible. In the
light of these observations it will therefore come as a surprise
to non-software specialists to learn that formal methods have
been around for a relatively long time (over 25 years) without
having made any significant impact on the world-wide community of
software developers. It is fair to say that there are more
textbooks on formal methods than there are documented case
studies of their use in real applications. In a sense the two new
books reviewed here, although both excellent in their own right,
highlight some of the reasons for this poor technology transfer.
In fact, formal methods (in various guises)
have been proposed since the early 1970's as a potential solution
to the software crisis. So why has there been so little take-up
of such an obviously good idea? A major reason, in my view, is
that that the wrong benefits have been emphasised. In particular,
proponents massively oversold the notion of proof of
correctness as the major motivation for using formal methods.
The idea was that, with formal methods, you could specify a
system in an appropriate formal notation and then prove
(in a mathematical sense) that a subsequent implementation of the
system was correct (with respect to the formal specification).
Proponents of formal methods argued (often persuasively) that
such an approach even circumvented the need for traditional
software testing. Thus, formal methods offered a potentially
revolutionary change to the way that software was developed and
tested. In practice, no complex systems have ever been developed
or proved correct in this way. In general it is infeasible to do
so. The other reason why I believe that formal methods have
failed to make the impact that they should have done is that the
formal notations themselves (of which there are several to choose
from) are too difficult for most practising software engineers to
use. In a recent article, leading expert Dave Parnas commented
that the formalists who set out to revolutionise software
development may have succeeded only in forming new research
cliques in computer science.
Despite these problems there is a growing
awareness that formal methods (including the existing non-perfect
variety) do have an important role to play, even if it is
restricted to the specification stage. The very act of producing
a formal specification can be beneficial in identifying
requirements faults. The formal specification notation that has
been used most widely in this sense is Z (which originated from
Oxford University Programming Research Group). It has also gained
widespread acceptance within the academic community. Woodcock and
Davies' book is the latest of several textbooks on Z. Woodcock is
a leading authority on Z and is also an excellent communicator.
Thus, as you would expect, this book is extremely well-written
and researched. Although there is a significant amount of
introductory material (sufficient for most Z courses) the
ultimate thrust of the book is related to the original motivation
for using formal methods: proving correctness. The authors have a
mission to show how Z can truly be used not just for
specification, but also for refinement and hence verification.
The material is not for the mathematically feint-hearted, but I
believe that the authors succeed in their goal. My concern is
that few students of this material will ever put into practice
the full method described here. The Z notation also features
heavily in the book by Hinchey and Bowen. This is a well edited
collection of case studies that will give readers useful insights
into practical applications of a range of notations (including
VDM, CCS and B-method). A collection like this is an important
milestone for the formal methods community. However, the
collection does little to dispel the view that real industrial
use of formal methods is extremely rare. For example, the most
convincing case study here is not a software system at all but a
microprocessor, while many of the other examples appear not to
have been used in earnest. Ultimately, I feel the desperately
sought technology transfer breakthrough will come only when there
is a body of empirical evidence to demonstrate the efficacy of
formal methods in both economic and quality terms. There is no
real evidence of this kind in either of these books. Hence their
usefulness is ultimately dependent on the empirical studies which
have only recently begun to appear.
You can contact me:-
by phone on +44 171 477 8425,
or by email as n.fenton@csr.city.ac.uk
.
Return To Norman Fenton's home page
- Go to the
City CSR Home Page.