[No longer publicly accessible] Design And Validation Of Computer Protocols

[No longer publicly accessible] Design And Validation Of Computer Protocols

Discusses the fundamental problems of designing logically consistent methods of communication between multiple computer processes. Standard protocol design problems, such as error control and flow control, are covered in detail.

Publication date: 31 Dec 1991

ISBN-10: 0135399254

ISBN-13: 0135399254

Paperback: 512 pages

Views: 38,403

Type: Textbook

Publisher: Prentice Hall

License: n/a

Post time: 05 Jan 2005 12:23:42

[No longer publicly accessible] Design And Validation Of Computer Protocols

[No longer publicly accessible] Design And Validation Of Computer Protocols Discusses the fundamental problems of designing logically consistent methods of communication between multiple computer processes. Standard protocol design problems, such as error control and flow control, are covered in detail.
Tag(s): Data Communication and Networks
Publication date: 31 Dec 1991
ISBN-10: 0135399254
ISBN-13: 0135399254
Paperback: 512 pages
Views: 38,403
Document Type: Textbook
Publisher: Prentice Hall
License: n/a
Post time: 05 Jan 2005 12:23:42
Update 10/11/2017:

The book in its entirety is no longer publicly accessible at Spinroot website. Only Chapter 1 and Chapter 8 remain so. The Download/View link has been updated.

From the Preface:

Protocols are sets of rules that govern the interaction of concurrent processes in distributed systems. Protocol design is therefore closely related to a number of established fields, such as operating systems, computer networks, data transmission, and data communications. It is rarely singled out and studied as a discipline in its own right. Designing a logically consistent protocol that can be proven correct, however, is a challenging and often frustrating task. It can already be hard to convince ourselves of the validity of a sequentially executed program. In distributed systems we must reason about concurrently executed, interacting programs.

Books about distributed systems, computer networks, or data communications often do no better than describe a set of standard solutions that have been accepted as correct by, for instance, large international organizations. They do not tell us why the solutions work, what problems they solve, or what pitfalls they avoid.

This text is intended as a guide to protocol design and analysis, rather than as a guide to standards and formats. It discusses design issues instead of applications. Two issues, therefore, are beyond the scope of this text: network control (including routing, addressing, and congestion control) and implementation. There is, however, no shortage of texts on both topics. The design problem is addressed here as a fundamental and challenging issue, rather than as an irritating practical obstacle to the development of reliable communication systems. The aim of the book is to make you familiar with all the issues of protocol validation and protocol design.

The first part of the book covers the basics. Chapter 1 gives a flavor of the types of problems that are discussed. Chapter 2 deals with protocol structure and general design issues. Chapters 3 and 4 discuss the basics of error control and flow control.

The next four chapters cover formal protocol modeling and specification techniques, beginning in Chapters 5 and 6 with the introduction of the concept of a protocol validation model, that serves as an abstraction of a design and a prototype of its implementation. In Chapter 5 a terse new language called PROMELA is introduced for the description of protocol validation models, and in Chapter 6 it is extended for the specification of protocol correctness requirements. In Chapter 7 we use PROMELA to discuss a number of standard design problems in the development of a sample file transfer protocol. Part II closes with a discussion, in Chapter 8, of the extended finite state machine, a basic notion in many formal modeling techniques.

The third part of the book focuses on protocol synthesis, testing, and validation techniques that can be used to battle a protocol’s complexity. Both the capabilities and the limitations of the formal design techniques are covered.

The fourth and last part of the book gives a detailed description of the design of two protocol design tools based on PROMELA: an interpreter and an automated validator. Based on these tools, an implementation generator is simple to add. Source code for the tools is provided in Appendices D and E. The source is also available in electronic form. Ordering information can be found in Appendix E.

Reviews:

Amazon.com

:) "In this one, Holzmann provides examples of protocols that look really simple while proving their correctness is utterly difficult. The examples are of particular interest for people working in networking."

:) "You have probably read the text from the back cover of the book, which is cited above. Every word of it is true. This is an excellent book, even for (serious) beginners, but also for experts who need some advice on how to avoid bad designs."
 




About The Author(s)


Gerard J. Holzmann (@gh_spin) is a Dutch-born American computer scientist and researcher at Bell Labs and NASA. Holzmann is known for the development of the SPIN model checker (SPIN is short for Simple Promela Interpreter) in the 1980s at Bell Labs. This device can verify the correctness of distributed software, since 1991 freely available. His specialities include software reliability, software verification techniques, image processing, and logic model checking.

Gerard J. Holzmann

Gerard J. Holzmann (@gh_spin) is a Dutch-born American computer scientist and researcher at Bell Labs and NASA. Holzmann is known for the development of the SPIN model checker (SPIN is short for Simple Promela Interpreter) in the 1980s at Bell Labs. This device can verify the correctness of distributed software, since 1991 freely available. His specialities include software reliability, software verification techniques, image processing, and logic model checking.


Book Categories
Sponsors
Icons8, a free icon pack