Book information

Applications of Formal Methods

Michael G. Hinchey & Jonathan P. Bowen (eds.)

Prentice Hall
International Series in Computer Science
1995

Applications of Formal Methods, Michael Hinchey and Jonathan Bowen (eds.). Prentice Hall International Series in Computer Science, series editor Prof. C.A.R. Hoare. 1995. ISBN 0-13-366949-1, Hardback cover,. xvii+447pp, UK£32.95 / US$57.95

See overview, Table of Contents, ordering information, reviews and related publications.

Overview

Interest in formal methods continues to grow; unfortunately myths and misconceptions regarding their benefits and application continue to grow also. Applications of Formal Methods is a collection of articles by internationally renowned contributors from both academia and industry which will dispel many of these myths.

Each of these essays illustrates the application of formal methods to realistic problems, each with an industrial relevance, in various application domains, describing how they can be scaled to large-scale problems, and providing an evaluation of methods, tools, and validation and verification techniques.

Key features include:

Foreword by C.A.R. Hoare;
Describes real-life examples of the application of formal methods, including descriptions of the methods used, and fragments of specifications which can be used in coursework;
Provides statistical evidence of the benefits of formal methods;
Discusses techniques for scaling formal methods for use at an industrial scale, and means of overcoming technology transfer problems;
Emphasizes tool support and the use of validation and verification techniques.

Applications of Formal Methods is essential reading for all students of formal methods and system development, as well as project managers considering the introduction of formal methods, and researchers in the field wishing to know more about industrial application and wishing to learn from the experiences of others.

From the foreword by C.A.R. Hoare:

The contribution of this book is exceptionally welcome, since it reports on a range of independent experiments in the application of theories on an industrial scale. In spite of diversity in the areas of application and in the formalisms selected, there is an encouraging uniformity in the overall conclusion: if appropriate attention is also paid to commercial, managerial and educational implications, there is a positive benefit to be achieved by increasing the level of formalism at the earliest possible stages of specification and design; and this benefit can be felt, if not measured, on the occasion of first use. There are grounds for optimism that second use may be even more beneficial.
That is why I regard the publication of this book as a milestone in the development of the series. It is a confirmation of the soundness of the goals that we have pursued in the past, and a promise of further achievement in the future.

Foreword by Prof. C.A.R. Hoare, Oxford University, UK.

Preface

Trademarks

List of Contributors

Michael G. Hinchey, New Jersey Institute of Technology (NJIT), USA / University of Limerick, Ireland & Jonathan P. Bowen, The University of Reading, UK
Applications of Formal Methods FAQ, pp 1-15.

David L. Parnas, McMaster University, Canada
Using Mathematical Models in the Inspection of Critical Software, pp 17-31.

Glenn Bruns & Stuart Anderson, University of Edinburgh, UK.
Gaining Assurance with Formal Methods, pp 33-54.

David Garlan, Carnegie-Mellon University, USA & Norman Delisle, Raytheon Corporation, USA
Formal Specification of an Architecture for a Family of Instrumentation Systems, pp 55-72.

Paul Mukherjee, Royal Holloway College, Univ. of London, UK & Brian A. Wichmann, National Physical Laboratory, UK
Formal Specification of the STV Algorithm, pp 73-96.

Jonathan Hoare, IBM UK Laboratories, UK
Application of the B-Method to CICS, pp 97-124.

Mandayam Srivas, SRI International, USA & Steve Miller, Rockwell International, USA
Formal Verification of the AAMP5 Microprocessor, pp 125-180.

William D. Young, Computational Logic Inc., USA
Modeling and Verification of a Simple Real-Time Gate Controller, pp 181-202.

Eugene H. Durr, Nico Plat & Michiel de Boer, CAP Volmac, The Netherlands
CombiCom: Tracking and Tracing Rail Traffic using VDM++, pp 203-226.

Babak Dehbonei & Fernando Mejia, GEC Alsthom, France
Formal Development of Safety-Critical Software Systems in Railway Signaling, pp 227-252.

Ute Hamer & Jan Peleska, DST Deutsche-System Technik GmbH, Germany
Z Applied to the A330/340 CIDS Cabin Communication System, pp 253-284.

David Guaspari, Mike Seager & Matt Stillerman, Odyssey Research Associates, USA
Specifying the Kernel of a Secure Distributed Operating System, pp 285-306.

Andrew Coombes, BAe Dependable Computing Systems Center, University of York, UK, Leonor Barroca, Open University, UK, John Fitzgerald, University of Manchester, UK John McDermid, BAe DCSC, University of York, UK, Lynne Spencer, BAe Warton, UK & Amer Saed, BAe DCSC, University of Newcastle-upon-Tyne, UK
Formal Specification of an Aerospace System: The Attitude Monitor, pp 307-332.

John Fitzgerald, University of Manchester, UK, Peter Gorm Larsen, IFAD, Denmark, Tom Brookes & Michael Green, British Aerospace (Systems and Equipment) Ltd., UK
Developing a Security-Critical System using Formal and Conventional Methods, pp 333-356.

This chapter reports on the work of the ConForm project.

Vivien Hamilton, Rolls-Royce & Associates, UK
The use of Z within a Safety-Critical Software System , pp 357-374.

Peter Mataga & Pamela Zave, AT&T Bell Laboratories, USA
Multiparadigm Specification of an AT&T Switching System, pp 375-398.

Dan Craigen, ORA Canada, Ottawa, Canada, Susan Gerhart, RICIS, University of Houston, USA & Ted Ralston, ORA, USA
Formal Methods Technology Transfer: Impediments and Innovation, pp 399-419.

Bibliography

Index

Ordering Information

Published 1995.

Order from your bookstore (e.g., Amazon.com Books (USA) from here), or directly from:

Prentice Hall
Campus 400
Maylands Avenue
Hemel Hempstead
Herts HP2 7EZ
UK

See also purchase information from Prentice Hall, including international orders.

Reviews

Letter from the Series Editor, 1996.

The main goal of the series has been to develop, illustrate and promulgate the scientic basis of computer programming, and its application in software engineering on an industrial scale. It is very encouraging to publish a record of success in this endeavour. Jonathan Bowen and Michael Hinchey have put together a varied collection of industrial case studies under the title Applications of Formal Methods. I hope they will be welcomed by the practitioner, removing some of the fear (but none of the challenge or benefit) of keeping to the forefront of the state of the art.
- Prof. Tony Hoare, Oxford University Computing Laboratory

Computer Weekly, 1 February 1996.

Heartily recommended and hopefully to be followed by more of the same.
- Peter Fox, Senior Consultant, EDS Ltd.

Times Higher Education Supplement, 13 September 1996.

Critical burden of being correct

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.
- Prof. Norman Fenton, Centre for Software Reliability, City University.

Related Publications

Ten Commandments of Formal Methods, J.P. Bowen and M.G. Hinchey. IEEE Computer, 28(4):56-63, April 1995. See also:
- Ten Commandments of Formal Methods. Technical Report No. 350, University of Cambridge Computer Laboratory, 18pp, September 1994.
Seven More Myths of Formal Methods, J.P. Bowen and M.G. Hinchey. IEEE Software, 12(4):34-41, July 1995. See also:
- Oxford University Computing Laboratory Technical Report PRG-TR-7-94, 19pp, June 1994.
- Seven More Myths of Formal Methods: Dispelling Industrial Prejudices. In M. Naftalin, T. Denvir and M. Bertran (eds), FME'94: Industrial Benefit of Formal Methods, Springer-Verlag, LNCS 873, pp 105-117, 1994.
- Seven More Myths of Formal Methods. Technical Report No. 357, University of Cambridge Computer Laboratory, 12pp, December 1994.
The Use of Industrial-Strength Formal Methods, J. P. Bowen and M. G. Hinchey. Proc. 21st International Computer Software & Application Conference (COMPSAC'97), Washington D.C., USA, 13-15 August 1997, pages 332-337, IEEE Computer Society Press, 1997.
Industrial-Strength Formal Methods, J. P. Bowen and M. G. Hinchey (eds.). Academic Press, International Series in Formal Methods, 1999.
High Integrity System Specification and Design, J. P. Bowen and M. G. Hinchey. Springer-Verlag, FACIT series, 1999.

See also information on formal methods. Many contributors are members of the ESPRIT ProCoS-WG Working Group.