📄 popd.html
字号:
<html> <head>
<title>Design and Validation of Computer Protocols</title>
</head>
<BODY BGCOLOR="#eeeeee" TEXT="#000000" LINK="#0000FF" VLINK="#330088" ALINK="#FF0044">
<img src=holzmann-popd.gif>
<h1>Design and Validation of Computer Protocols</h1>
<p>
<i>Design and Validation of Computer Protocols</i>
by Gerard J. Holzmann, was published by Prentice Hall in November 1990.
Among others, it details the design and implementation of
the Spin model checking system.
<p>
The book can be ordered in paperback from online booksellers such
as <a href="http://www.amazon.com/">www.amazon.com</a>.
<br>
The book contents is also available online via:
<pre>
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Doc/Book91.html">http://cm.bell-labs.com/cm/cs/what/spin/Doc/Book91.html</a>
</pre>
<p>
<ul>
<li><A NAME=1 HREF="#Synopsis">Synopsis of book</A>
<li><A NAME=2 HREF="#Contents">Complete table of contents</A>
<li><A NAME=3 HREF="#Foreword">Foreword by Colin West</A>
</ul>
<p>
<p>
ISBN 0-13-539925-4 hardcover (USA)
<br>
ISBN 0-13-539834-7 paperback (international edition)
<p>
<A NAME="Synopsis">
<h1>Synopsis</h1>
<p>
The book introduces a sound discipline for the design of complete
and consistent concurrent systems.
The techniques explored in this book have been applied to
the design of distributed systems, operating systems,
telephone switching systems, and network protocols,
but they are not restricted to any particular application.
With the validation tools presented in this book,
formal validations of industrial-size problems
can be performed effectively.
<p>
The first part of the book gives the reader an overview
of the types of fundamental coordination problems that
a protocol designer must be able to recognize.
It covers the basics of error control, flow control, and
protocol structuring, and presents ten basic rules of protocol design.
Part two covers protocol specification and modeling techniques,
and introduced the notion of a protocol validation model.
Part three gives an overview of protocol synthesis, conformance
testing, manual and automated protocol validation techniques.
In the final part of the book a detailed description is given
of a set of tools that can be used to attack the protocol
design problem in a rigorous and practical manner.
Complete source code for the tools is provided.
<p>
<A NAME="Contents">
<h1>Table of Contents</h1>
<h2>Foreword ix</h2>
<h2>Preface xi</h2>
<p>
<h2>Part I -- Basics</h2>
<h1>1. Introduction</h1>
<ul>
<li>1.1 Early Beginnings 1
<li>1.2 The First Networks 9
<li>1.3 Protocols as Languages 12
<li>1.4 Protocol Standardization 13
<li>1.5 Summary 15
<li>Exercises 16
<li>Bibliographic Notes 17
</ul>
<p>
<h2>2. Protocol Structure</h2>
<ul>
<li>2.1 Introduction 19
<li>2.2 The Five Elements of a Protocol 21
<li>2.3 An Example 22
<li>2.4 Service and Environment 27
<li>2.5 Vocabulary and Format 32
<li>2.6 Procedure Rules 35
<li>2.7 Structured Protocol Design 36
<li>2.8 Ten Rules of Design 39
<li>2.9 Summary 40
<li>Exercises 40
<li>Bibliographic Notes 41
</ul>
<p>
<h2>3. Error Control</h2>
<ul>
<li>3.1 Introduction 43
<li>3.2 Error Model 44
<li>3.3 Types of Transmission Errors 46
<li>3.4 Redundancy 46
<li>3.5 Types of Codes 47
<li>3.6 Parity Check 48
<li>3.7 Error Correction 49
<li>3.8 A Linear Block Code 52
<li>3.9 Cyclic Redundancy Checks 57
<li>3.10 Arithmetic Checksum 63
<li>3.11 Summary 64
<li>Exercises 65
<li>Bibliographic Notes 66
</ul>
<p>
<h2>4. Flow Control</h2>
<ul>
<li>4.1 Introduction 67
<li>4.2 Window Protocols 71
<li>4.3 Sequence Numbers 75
<li>4.4 Negative Acknowledgments 82
<li>4.5 Congestion Avoidance 84
<li>4.6 Summary 88
<li>Exercises 88
<li>Bibliographic Notes 90
</ul>
<p>
<h1>Part II -- Specification and Modeling</h1>
<h2>5. Validation Models</h2>
<ul>
<li>5.1 Introduction 91
<li>5.2 Processes, Channels, Variables 92
<li>5.3 Executability of Statements 92
<li>5.4 Variables and Data Types 93
<li>5.5 Process Types 94
<li>5.6 Message Channels 98
<li>5.7 Control Flow 101
<li>5.8 Examples 104
<li>5.9 Modeling Procedures and Recursion 105
<li>5.10 Message Type Definitions 106
<li>5.11 Modeling Timeouts 106
<li>5.12 Lynch's Protocol Revisited 107
<li>5.13 Summary 109
<li>Exercises 109
<li>Bibliographic Notes 111
</ul>
<p>
<h2>6. Correctness Requirements</h2>
<ul>
<li>6.1 Introduction 112
<li>6.2 Reasoning about Behavior 113
<li>6.3 Assertions 116
<li>6.4 System Invariants 116
<li>6.5 Deadlocks 118
<li>6.6 Bad Cycles 119
<li>6.7 Temporal Claims 120
<li>6.8 Summary 126
<li>Exercises 126
<li>Bibliographic Notes 127
</ul>
<p>
<h2>7. Protocol Design</h2>
<ul>
<li>7.1 Introduction 128
<li>7.2 Service Specification 129
<li>7.3 Assumptions about the Channel 130
<li>7.4 Protocol Vocabulary 131
<li>7.5 Messsage Format 133
<li>7.6 Procedure Rules 141
<li>7.7 Summary 160
<li>Exercises 161
<li>Bibliographic Notes 162
</ul>
<p>
<h2>8. Finite State Machines</h2>
<ul>
<li>8.1 Introduction 163
<li>8.2 Informal Description 163
<li>8.3 Formal Description 171
<li>8.4 Execution of Machines 172
<li>8.5 Minimization of Machines 173
<li>8.6 The Conformance Testing Problem 176
<li>8.7 Combining Machines 176
<li>8.8 Extended Finite State Machines 177
<li>8.9 Generalization of Machines 180
<li>8.10 Restricted Models 183
<li>8.11 Summary 186
<li>Exercises 187
<li>Bibliographic Notes 187
</ul>
<p>
<h1>Part III -- Conformance Testing, Synthesis and Validation</h1>
<h2>9. Conformance Testing</h2>
<ul>
<li>9.1 Introduction 189
<li>9.2 Functional Testing 190
<li>9.3 Structural Testing 191
<li>9.4 Deriving UIO Sequences 197
<li>9.5 Modified Transition Tours 199
<li>9.6 An Alternative Method 199
<li>9.7 Summary 201
<li>Exercises 202
<li>Bibliographic Notes 203
</ul>
<p>
<h2>10. Protocol Synthesis</h2>
<ul>
<li>10.1 Introduction 206
<li>10.2 Protocol Derivation 206
<li>10.3 Derivation Algorithm 211
<li>10.4 Incremental Design 213
<li>10.5 Place Synchronization 213
<li>10.6 Summary 214
<li>Exercises 215
<li>Bibliographic Notes 215
</ul>
<p>
<h2>11. Protocol Validation</h2>
<ul>
<li>11.1 Introduction 217
<li>11.2 Manual Proof Method 217
<li>11.3 Automated Validation Methods 221
<li>11.4 The Supertrace Algorithm 230
<li>11.5 Detecting Non-Progress Cycles 235
<li>11.6 Detecting Acceptance Cycles 238
<li>11.7 Checking Temporal Claims 239
<li>11.8 Complexity Management 240
<li>11.9 Boundedness of PROMELA Models 242
<li>11.10 Summary 243
<li>Exercises 244
<li>Bibliographic Notes 244
</ul>
<p>
<h1>Part IV -- Design Tools</h1>
<h2>12. A Protocol Simulator</h2>
<ul>
<li>12.1 Introduction 247
<li>12.2 SPIN -- Overview 248
<li>12.3 Expressions 249
<li>12.4 Variables 259
<li>12.5 Statements 269
<li>12.6 Control Flow 278
<li>12.7 Process and Message Types 285
<li>12.8 Macro Expansion 294
<li>12.9 SPIN Options 295
<li>12.10 Summary 297
<li>Exercises 298
<li>Bibliographic Notes 298
</ul>
<p>
<h2>13. A Protocol Validator</h2>
<ul>
<li>13.1 Introduction 298
<li>13.2 Structure of the Validator 299
<li>13.3 The Validation Kernel 300
<li>13.4 The Transition Matrix 303
<li>13.5 The Validator-Generator Code 305
<li>13.6 Overview of the Code 308
<li>13.7 Guided Simulation 310
<li>13.8 Some Applications 311
<li>13.9 Coverage in Supertrace Mode 315
<li>13.10 Summary 316
<li>Exercises 316
<li>Bibliographic Notes 317
</ul>
<p>
<h2>14. Using the Validator</h2>
<ul>
<li>14.1 Introduction 318
<li>14.2 An Optical Telegraph Protocol 318
<li>14.3 Dekker's Algorithm 320
<li>14.4 A Larger Validation 322
<li>14.5 Flow Control Validation 325
<li>14.6 Session Layer Validation 336
<li>14.7 Summary 348
<li>Exercises 349
<li>Bibliographic Notes 349
</ul>
<p>
<h2>Conclusion 350</h2>
<h2>References 351</h2>
<h2>Appendices</h2>
<ul>
<li>A. Data Transmission 369
<li>B. Flow Chart Language 382
<li>C. PROMELA Language Report 385
<li>D. SPIN Simulator Source 394
<li>E. SPIN Validator Source 433
<li>F. PROMELA File Transfer Protocol 483
<p>
<li>Name Index 491
<li>Subject Index 493
</ul>
<p>
<A NAME="Foreword">
<h1>Foreword by Colin West</h1>
<p>
It is now over 15 years since the first, tentative efforts were made
to assemble theories and tools that could help with the development of
communications protocols \(en the rules and procedures that control and
manage the flow of information within computer networks.
During the intervening years, a significant body of knowledge has
been accumulated that can be successfully applied to the various
phases of protocol development. There are now international standards
for languages designed for the formal specification of the protocols
upon which we will build our future computer networks. We have
learned that even the most carefully developed protocol specifications
contain subtle errors unless they are subjected to a thorough error
analysis. Much progress has been made in the development of automated
tools to support this. There have also been significant advances in
testing techniques that make it possible to build reliable
heterogeneous networks using hardware and software from a wide
spectrum of manufacturers and development organizations.
<p>
We are fortunate that Gerard Holzmann has made the effort to write
this book that summarizes much of what we know about designing
protocols and documents his own considerable experience in the field.
His book has four major sections. The first gives an introduction to
the problems that are encountered during the development of protocols
and discusses the principles of protocol design. The historical
examples used to introduce the subject are a delight. The second
section discusses ways in which a protocol can be modeled and
specified. The third explains how protocol models can be analyzed to
determine their properties and evaluate their correctness. The final
section presents protocol design tools which complement the material
in the earlier sections of the book. This is an important section.
Protocols have proved to be extremely difficult to understand without
automated analysis tools. The serious student of the field will learn
a great deal by using the tools presented here to build and analyze
his own protocols.
<p>
<address><A HREF="/cm/cs/who/gerard/">
Gerard J. Holzmann, </A>
gerard@bell-labs.com</address>
<br>
</body> </html>
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -