Автор: Gerard J. Holzmann
Название: Design And Validation Of Computer Protocols
Издательство: Prentice Hall
Год: 1991
ISBN: 0135399254
Серия: Prentice Hall Software Series
Язык: English
Формат: pdf
Размер: 1,3 mb
Страниц: 512

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 conect. 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.

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.

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 selves 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, hi 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.