A Case Study: the Mini-PABX
One of the most interesting case studies we made is the formal specification of a substantial part of a call handling system, the ITT 5400 BCS (Business Communication System) [Bell85b]. The ITT 5400 BCS is a modern Private Automatic Branch Exchange (PABX
- PDF / 48,301,862 Bytes
- 362 Pages / 481.89 x 685.98 pts Page_size
- 82 Downloads / 243 Views
Algebraic Specifications in Software Engineering An Introduction
With 240 Figures
Springer-Verlag Berlin Heidelberg New York London Paris Tokyo Hong Kong
Ivo Van Horebeek lohan Lewi Katholieke Universiteit Leuven Department of Computer Science Celestijnenlaan 200 A B-3030 Leuven/Heverlee, Belgium
ISBN-13: 978-3-642-75032-8 001: 10.1007/978-3-642-75030-4
e-ISBN-13: 978-3-642-75030-4
Library of Congress Cataloging-in-Publication Data Horebeek, Ivo van, 1959- Algebraic specifications in software engineering: an introduction Ivo van Horebeek, Johan Lewi. p. cm. Includes bibliographical references. l. Software engineering. 2. Abstract data types (Computer science) I. Lewi, Johan. II. Title. QA 76. 758.H67 1989 005.1'01'5102--dc20 89-26115
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broad-casting, reproduction on microfilms or in other ways, and storage in data banks. Duplication of this publication or parts thereof is only permitted under the provisions of the German Copyright Law of September 9, 1965, in its version of June 24, 1985, and a copyright fee must always be paid. Violations fall under the prosecution act of the German Copyright Law.
© Springer-Verlag Berlin Heidelberg 1989 Softcover reprint of the hardcover 15t edition 1989 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 protective laws and regulations and therefore free for general use. Offsetprinting: Weihert-Druck GmbH, Darmstadt Binding: J. Schaffer GmbH & Co. KG, Griinstadt 2145/3140-543210
To Lutgarde and Dany
Preface "I prefer to view formal methods as tools. the use of which might be helpful." E. W. Dijkstra
Algebraic specifications are about to be accepted by industry. Many projects in which algebraic specifications have been used as a design tool have been carried out. What prevents algebraic specifications from breaking through is the absence of introductory descriptions and tools supporting the construction of algebraic specifications. On the one hand. interest from industry will stimulate people to make introductions and tools. whereas on the other hand the existence of introductions and tools will stimulate industry to use algebraic specifications. This book should be seen as a contribution towards creating this virtuous circle. The book will be of interest to software designers and programmers. It can also be used as material for an introductory course on algebraic specifications and software engineering at undergraduate or graduate level. Nowadays. there is general agreement that in large software projects appropriate specifications are a must in order to obtain quality software. Informal specifications alone are certainly not appropriate because they are incomplete. inconsistent. inaccurate and ambiguous and they rapidly become bulky and therefore u
