英语论文网

DESIGN AND VALIDATIONOF COMPUTER PROTOCOLS
Gerard J. Holzmann
Bell Laboratories
Murray Hill, New Jersey 07974
PRENTICE-HALL
Englewood Cliffs, New Jersey 07632
代写留学生博士论文Prentice Hall Software Series
Brian W. Kernighan, Advisor
Copyright 1991 by Lucent Technologies, Bell Laboratories, Incorporated.
This book is typeset in Times Roman by the author,
using an Linotronic 200P phototypesetter and a DEC VAX 8550
running the 10th Edition of the UNIXoperating system.
DEC and VAX are trademarks of Digital Equipment Corporation.
UNIX is a registered trademark of AT&T.
All rights reserved.
No part of this publication may be reproduced, stored in a retrieval system,
or transmitted, in any form or by any means, electronic,
mechanical, photocopying, recording, or otherwise,
without the prior written permission of the publisher.
Printed in the United States of America
10 9 8 7 6 5 4 3 2 1
Prentice-Hall International (UK) Limited, London
Prentice-Hall of Australia Pty. Limited, Sydney
Prentice-Hall Canada Inc., Toronto
Prentice-Hall Hispanoamericana, S.A., Mexico
Prentice-Hall of India Private Limited, New Delhi
Prentice-Hall of Japan, Inc., Tokyo
Simon & Schuster Asia Pte. Ltd., Singapore
Editora Prentice-Hall do Brasil, Ltda., Rio de Janeiro
CONTENTS
Foreword ix
Preface xi
Part I — Basics
1. Introduction
1.1 Early Beginnings 1
1.2 The First Networks 9
1.3 Protocols as Languages 12
1.4 Protocol Standardization 13
1.5 Summary 15
Exercises 16
Bibliographic Notes 16
2. Protocol Structure
2.1 Introduction 19
2.2 The Five Elements of a Protocol 21
2.3 An Example 22
2.4 Service and Environment 26
2.5 Vocabulary and Format 32
2.6 Procedure Rules 35
2.7 Structured Protocol Design 35
2.8 Ten Rules of Design 38
2.9 Summary 39
Exercises 39
Bibliographic Notes 40
3. Error Control
3.1 Introduction 43
3.2 Error Model 44
3.3 Types of Transmission Errors 46
3.4 Redundancy 46
3.5 Types of Codes 47
3.6 Parity Check 48
3.7 Error Correction 48
3.8 A Linear Block Code 52
3.9 Cyclic Redundancy Checks 56
3.10 Arithmetic Checksum 63
3.11 Summary 64
Exercises 64
Bibliographic Notes 65
4. Flow Control
4.1 Introduction 66
4.2 Window Protocols 70
4.3 Sequence Numbers 74
4.4 Negative Acknowledgments 80
4.5 Congestion Avoidance 83
4.6 Summary 86
Exercises 87
Bibliographic Notes 88
Part II — Specification and Modeling
5. Validation Models
5.1 Introduction 90
5.2 Processes, Channels, Variables 91
5.3 Executability of Statements 91
5.4 Variables and Data Types 92
5.5 Process Types 93
5.6 Message Channels 96
5.7 Control Flow 100
5.8 Examples 102
5.9 Modeling Procedures and Recursion 104
5.10 Message Type Definitions 104
5.11 Modeling Timeouts 105
5.12 Lynch’s Protocol Revisited 106
5.13 Summary 107
Exercises 108
Bibliographic Notes 109
6. Correctness Requirements
6.1 Introduction 111
6.2 Reasoning about Behavior 112
6.3 Assertions 114
6.4 System Invariants 115
6.5 Deadlocks 117
6.6 Bad Cycles 118
6.7 Temporal Claims 119
6.8 Summary 125
Exercises 126
Bibliographic Notes 127
7. Protocol Design
7.1 Introduction 128
7.2 Service Specification 129
7.3 Assumptions about the Channel 130
7.4 Protocol Vocabulary 131
7.5 Messsage Format本论文由英语论文网提供整理，提供论文代写，英语论文代写，代写论文，代写英语论文，代写留学生论文，代写英文论文，留学生论文代写相关核心关键词搜索。