Milestone for the maths community

Norman Fenton recommends a collection of applied formal-methods studies.

Formal methods is the term by which computer scientists refer to the use of mathematics in system specification and development. A major rationale for using formal (as opposed to informal) methods of specification and development is to be able to reason formally about properties of a system before expensive design and coding has begun. This way it may be possible to identify and fix requirements problems that so plague complex software projects. Another rationale for using formal methods is that they potentially enable us to prove that a system is correct with respect to its specification.

Although the "proof of correctness" rationale has been an over-sold aspect of formal methods - where "proofs" exist at all, they tend to be informal - there is an increasing realisation that formal methods for specification are an important component of best-practice software engineering. This is especially the case for applications that are safety or business critical.

This very well-edited, nicely introduced collection of case studies confirms that formal methods are being used quite seriously in such applications. Indeed I agree with the view of Michael Jackson, who asserts in the foreword: "Both experience and advocacy of formal methods are coming of age. This book is a rich record of much that has been learned in the progression from the naivete of childhood to the practical common sense of more mature years."

When I reviewed the authors' earlier edited collection of formal-methods case studies Applications of Formal Methods , in The THES , (September 13 1996) I made the following remarks: "This is a well-edited collection of case studies that will give readers useful insights into practical applications of a range of notations 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."

My concerns were due to the fact that the most convincing case study in the book was not a software system at all but a micro-processor, while many of the other examples appeared not to have been used in earnest.

The current collection is more convincing, although again in some of these studies the described systems do not appear to have been built and/or used.

For example, one study by Dines Bjørner and colleagues uses the Raise method to specify and develop a prototype scheduling system for the Chinese railways.

Bjørner asserts in the conclusion that the study provides evidence to counter the claims that formal methods are expensive and difficult. However, reading between the lines it seems that the Chinese railways were using the project merely as a software-engineering learning exercise and later on we discover that "the project stopped very abruptly".

Much more convincing is the study by John Jacky of the control software for a radiation therapy machine. This was a real system in which the author was the problem owner (and was not originally a formal-methods expert). The author learned and used Z and is able to provide some very useful insights into both the advantages and disadvantages of formal methods. Overall, he is very positive about the experience and as such this presents a more impressive case study than the type that are written up by academic onlookers.

There are in total 15 chapters, of which (in my view) eight describe in reasonable detail the use of some formal method on systems that were built and at least partly used. In addition to Jacky's study these are: Pascal Bernard and Guy Laffitte (B method used for part of the system of the French population census of 1990); Ross Anderson (extension of BAN logic used for the formal verification of an electronic payment system); Bishop Brock and Warren Hunt (ACL-2 logic used for formal specification of a digital signal processor for Motorola); Yonit Kesten et al (linear temporal logic used in the verification of an e-commerce internet security server); Anthony Hall (VDM used in an air traffic-control application); Andrew Moore et al (a CSP-type approach to a network security device); Arne Boralv and Gunnar Stalmarck (who describe a range of methods used in Swedish railways projects). There are two chapters (including the one by Bjørner) that describe prototype or mythical systems (the other is by Kevin Lano et al who use B to specify a chemical process controller). There are four chapters that describe methodological approaches to formal methods without specific case studies (for example, one by Nancy Leveson et al , describes a CAD environment used for a range of safety-critical software). There is one chapter (by Dan Craigen et al ) that focuses on a tool for analysing Z specifications.

The range of formal methods used in this book will no doubt encourage some potential readers and discourage others. It is doubtful that the book could be used as the main text for a formal-methods course. But, with its strong supporting material, it is the best collection of applied formal methods I have seen.

Norman Fenton is professor of computing science, City University.