Formal Approaches to Computing and Information Technology Springer London Berlin Heidelberg New York Barcelona Hong Kong Milan Paris Santa Clara Singapore Tokyo Also in this series: Proof in VDM: A Practitioner's Guide J.e. Bicarregui, J.S. Fitzgerald, P.A. Lindsay, R. Moore and B. Ritchie ISBN 3-540-19813-X The B Language and Method K.Lano ISBN 3-540-76033-4 A Theory and Practice of Program Development D.Andrews ISBN 3-540-76162-4 Constructing Correct Software: the basics J. Cooke ISBN 3-540-76156-X Formal Methods in Human-Computer Interaction P. Palanque and F. Paterno (Eds) ISBN 3-540-76158-6 Proof in VDM: Case Studies J.C. Bicarregui (Ed.) ISBN 3-540-76186-1 Program Development by Refinement E. Sekerinski and K. Sere (Eds) ISBN 1-85233-053-8 Jonathan P. Bowen and Michael G. Hinchey High-Integrity System Specification and Design , Springer Jonathan P. Bowen, BA, MA Department of Computer Science, University of Reading, P.O. Box 225, Whiteknights, Reading, Berkshire, RG6 6AY, UK Michael G. Hinchey, BSc, MSc, PhD Department of Computer Science, University of Nebraska-Omaha, College of Information Science and Technology, 6001 Dodge Street, Omaha, NE 68182-0500, USA Series Editor S.A. Schuman, BSc, DEA, CEng Department of Mathematical and Computing Sciences University of Surrey, Guildford, Surrey GU2 5XH, UK ISBN-13: 978-3-540-76226-3 e-ISBN-13: 978-1-4471-3431-2 DOl: 10.1007/978-1-4471-3431-2 British Library Cataloguing in Publication Data A catalogue record for this book is available from the British Library Library of Congress Cataloging-in-Publication Data High-integrity system specification and design 1 Jonathan P. Bowen and Michael G. Hinchey. p. cm. -- (Formal approaches to computing and information technology) Includes bibliographical references and index. 1. System design. 2. System analysis. I. Bowen, J.P. (jonathan Peter), 1956- . II. Hinchey, Michael G. (Michael Gerard), 1969- . III. Series. QA76.9.S88H52 1998 98-50694 004.2' 1--dc21 CIP Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of repro graphic reproduction in accordance with the terms oflicences issued by the Copyright Licensing Agency. Enquiries concerning reproduction outside those terms should be sent to the publishers. © Springer-Verlag London Limited 1999 The use of registered names, trademarks etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant laws and regulations and therefore free for general use. The publisher makes no representation, express or implied, with regard to the accuracy of the information contained in this book and cannot accept any legal responsibility or liability for any errors or omissions that may be made. Typesetting: Camera ready by authors 34/3830-543210 Printed on acid-free paper There are two ways of constructing a software design. One way is to make it so simple that there are obviously no defi ciencies. And the other way is to make it so complicated that there are no obvious deficiencies. - C.A.R. Hoare Preface Errata, detected in Taylor's Logarithms. London: 4to, 1792. [sic] 6 Kk Co-sine of 14.18.3 3398 3298 - Nautical Almanac (1832) In the list of ERRATA detected in Taylor's Logarithms, for cos. 4° 18'3", read cos. 14° 18'2". - Nautical Almanac (1833) ERRATUM ofthe ERRATUM ofthe ERRATA of TAYLOR'S Logarithms. For cos. 4° 18'3", read cos. 14° 18' 3". - Nautical Almanac (1836) In the 1820s, an Englishman named Charles Babbage designed and partly built a calculating machine originally intended for use in deriving and printing logarithmic and other tables used in the shipping industry. At that time, such tables were often inaccurate, copied carelessly, and had been instrumental in causing a number of maritime disasters. Babbage's machine, called a 'Difference Engine' because it performed its cal culations using the principle of partial differences, was intended to substantially reduce the number of errors made by humans calculating the tables. Babbage had also designed (but never built) a forerunner of the modern printer, which would also reduce the number of errors admitted during the transcription of the results. Nowadays, a system implemented to perform the function of Babbage's engine would be classed as safety-critical. That is, the failure of the system to produce correct results could result in the loss of human life, mass destruction of property (in the form of ships and cargo) as well as financial losses and loss of competitive advantage for the shipping firm. Computer systems now influence almost every facet of our lives. They wake us up in the morning, control the cooking of our food, entertain us, help in avoid ing traffic congestion and control the vehicles in which we travel, they wash our clothes, and even give us cash from our bank accounts (sometimes!). Increasingly, they are being used in systems where they can have a great influence over our very existence. They control the flow of trains in the subway, signaling on railway lines, even traffic lights on the street. The failure of any of these systems would cause us viii High-Integrity System Specification and Design great inconvenience, and could conceivably result in accidents in which lives may be lost. As they control the actual flight of an airplane, cooling systems in chemical plants, feedback loops in nuclear power stations, etc., we can see that they allow the possibility of great disasters if they fail to operate as expected. In recent years, the media, in the form of both television news and the popular science journals, have become very preoccupied with the failures of a number of safety-critical computer systems. A number of systems, or classes of system, seem to have particularly caught their attention; chief amongst these are various nuclear power plants where the cooling systems or shutdown loops have been demonstrated to be inconsistent, and recent air crashes which cannot be convincingly blamed on pilot error. The introduction of computer systems to replace more traditional mechanical systems (consider, for example, Boeing's fly-by-wire system in the 777 jet, and the disastrous baggage-handling system at Denver airport) has made both the system development community and the general public more aware of the unprecedented opportunities for the introduction of errors that computers admit. Many journalists have become self-styled authorities on techniques that will give greater confidence in the correctness of complex systems, and reduce the number and frequency of computer errors. High-Integrity Systems, or systems whose code is relied upon to be of the highest quality and error-free, are often both security-and safety-critical in that their failure could result in great financial losses for a company, mass destruction of property and the environment, and loss of human life. Formal Methods have been widely advocated as one of those techniques which can result in high-integrity systems, and their usage is being suggested in an increasing number of standards in the safety-critical domain. Notwithstanding that, formal methods re main one of the most controversial areas of modern software engineering practice. They are the subject of extreme hyperbole by self-styled 'experts' who fail to un derstand what formal methods actually are, and of deep criticism by proponents of other techniques who see formal methods as merely an opportunity for academics to exercise their intellects over whichever notation is the current 'flavor-of-the-month'. This book serves as an introduction to the task of specification and design of high-integrity systems, with particular attention paid to formal methods throughout, as these (in our opinion) represent the most promising development in this direction. We do not claim that this book will tell the reader everything he/she needs to know, but we do hope that it will help to clarify the issues, and give a good grounding for further investigation. Each of the major Parts of the book consists of expository material, couched at levels suitable for use by computer science and software engineering students (both undergraduate and graduate), giving an overview of the area, pointers to additional material, and introductions to the excellent papers which are reprinted in this vol ume. For practicing software engineers too, both industrialists and academics, this book should prove to be of interest. It brings together some of the 'classic' works in Preface ix the field, making it an interesting book of readings for self-study, and a convenient, comprehensive reference. Part 1 introduces the many problems associated with the development of large scale systems, describes the system life-cycle, and suggests potential solutions which have been demonstrated to be particularly promising. Traditionally, computer systems have been analyzed, specified and designed using a number of diagrammatic techniques. Over the years, different techniques and notations have been combined into various structured methods of development. These are introduced in Part 2, and a number of the more popular methods are de scribed. Part 3 goes on to describe formal methods, the major focus of this collection. The components of a formal method are identified; overviews of several representative formal methods are given, and major misconceptions regarding formal methods are identified and dispelled. Object-Orientation has often been cited as a means of aiding in reducing com plexity in system development. Part 4 introduces the subject, and discusses issues related to object-oriented development. With increased performance requirements, and greater dispersal of processing power, concurrent and distributed systems have become very prevalent. Their de velopment, however, can be exponentially more difficult than the development of traditional sequential systems. Part 5 discusses such issues, and describes two di verse approaches to the development of such systems. Increasingly, complex concurrent and distributed systems are employed in ar eas where their use can be deemed to be safety-critical, and where they are relied upon to perform within strict timing constraints. Part 6 identifies the relationship of formal methods to safety-critical standards and the development of safety-critical systems. The appropriateness of a number of formal methods is discussed, and some interesting case studies are presented. While formal methods have much to offer, many fail to address the more methodological aspects of system development. In addition, there has been consid erable effort invested in the development of appropriate structured methods which it would be foolhardy to ignore. Part 7 presents the motivation for integrating struc tured and formal methods, as a means of exploiting the advantages of each. Clearly the aim of system development is to derive a sensible implementation of the system that was specified at the outset. Part 8 introduces refinement of for mal specifications, rapid prototyping and simulation, and the relative merits of exe cutable specifications. Part 9 addresses the mechanization of system development, and tool support via Computer-Aided Software Engineering (CASE). The future of CASE, and the advent of 'visual formalisms', exploiting graphical representation with formal un derpinnings, is postulated. Finally, a bibliography with recent references is included for those wishing to follow up on any of the issues raised in more depth. We hope this collection of papers and articles, together with the associated commentary, provide food for thought to x High-Integrity System Specification and Design all those actively involved in or contemplating the production of computer-based high integrity systems. Information associated with this book will be maintained on-line under the fol lowing URL (Uniform Resource Locator): http://www.fmse.cs.reading.ac.uk/hissd/ Relevant developments subsequent to publication of this collection will be added to this resource. I.P.B. M.G.H. Reading Omaha Table of Contents Acknowledgements. .. . . . . .. .. . . .. . . .. .. . . . . . . . . .. . . . . .. . ... .. . .. xv List of Reprints ................................................. xvii 1. Specification and Design. . . . . . . . . . . . . . . . . . . . . . . . . . ........... . 1.1 An Analogy. .. . .. .. .. . .. .. ... .. ... . . .. ... . . . .. .. .. . . ... . . . 1 1.2 The Development Life-Cycle. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 The Transformational Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.4 Silver Bullets. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 No Silver Bullet: Essence and Accidents of Software Engineering (Brooks) 11 Biting the Silver Bullet: Toward a Brighter Future for System Develop- ment (Harel) ............................ .-. . . . . . . . . . . . . . . . .. 29 2. Structured Methods .......................... . . . . . . . . . . . . . .. 53 2.1 Structured Notations. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 53 2.2 The Jackson Approach ...................................... 54 Methodology: The Experts Speak (Orr, Gane, Yourdon, Chen & Con- stantine) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 57 An Overview of JSD (Cameron) ................................... 77 3. Formal Methods ............................................ 127 3.1 What are Formal Methods? .................................. 128 3.2 Formal Specification Languages .............................. 128 3.3 Deductive Apparatus ........................................ 129 3.4 Myths of Formal Methods ................................... 130 3.5 Which Formal Method? ..................................... 131 Seven Myths of Formal Methods (Hall) ............................. 135 Seven More Myths of Formal Methods (Bowen & Hinchey) ............ 153 A Specifier's Introduction to Formal Methods (Wing) ................. 167 An Overview of Some Formal Methods for Program Design (Hoare) ..... 201 Ten Commandments of Formal Methods (Bowen & Hinchey) ........... 217