Applications of Formal Methods
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
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.
Table of contents
List of contributors
Jonathan Hoare, IBM UK Laboratories, UK
Application of the B-Method to CICS, pp 97–124.
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.
Herts HP2 7EZ
Letter from the Series Editor, 1996.
The main goal of the series has been to develop, illustrate and promulgate the scientific 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.
Computer Weekly, 1 February 1996.
— Peter Fox, Senior Consultant, EDS Ltd.
Times Higher Education Supplement, 13 September 1996.
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.
- Ten Commandments of Formal Methods, J.P. Bowen and M.G. Hinchey. IEEEComputer, 28(4):56-63, April 1995. See also:
- Seven More Myths of Formal Methods, J.P. Bowen and M.G. Hinchey. IEEESoftware, 12(4):34-41, July 1995. See also:
Seven More Myths of Formal Methods</A>. <A HREF= 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 in Practice, J. P. Bowen and M. G. Hinchey (eds.). Springer-Verlag, FACIT series, 1999.
- High-Integrity System Specification and Design, J. P. Bowen and M. G. Hinchey. Springer-Verlag, FACIT series, 1999.