Design and Validation of Computer Protocol.pdf

发布时间：2022-06-09 发布人：admin 分类：说明书资料大小：2.07M 资料格式：pdf 举报版权申诉

anilji-4645822-4744300845382455205.pdf-第1页.png

第1页 / 共558页

anilji-4645822-4744300845382455205.pdf-第2页.png

第2页 / 共558页

anilji-4645822-4744300845382455205.pdf-第3页.png

第3页 / 共558页

anilji-4645822-4744300845382455205.pdf-第4页.png

第4页 / 共558页

anilji-4645822-4744300845382455205.pdf-第5页.png

第5页 / 共558页

anilji-4645822-4744300845382455205.pdf-第6页.png

第6页 / 共558页

anilji-4645822-4744300845382455205.pdf-第7页.png

第7页 / 共558页

anilji-4645822-4744300845382455205.pdf-第8页.png

第8页 / 共558页

preface

contents

ch1

ch2

ch3

ch4

ch5

ch6

ch7

ch8

ch9

ch10

ch11

ch12

ch13

ch14

conclusion

references

appA

appB

appC

appD

appE

appF

name_index

subject_index

DESIGN AND VALIDATION COMPUTER PROTOCOLS Gerard J. Holzmann -----------, OF PRENTICE HALL SOFTWARE SERI ES www.spinroot.com

DESIGN AND VALIDATION OF COMPUTER PROTOCOLS Gerard J. Holzmann Bell Laboratories Murray Hill, New Jersey 07974 PRENTICE-HALL Englewood Cliffs, New Jersey 07632 www.spinroot.com

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. No part of this publication may be reproduced, stored in a retrieval system, All rights reserved. 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 www.spinroot.com

Foreword Preface Part I — Basics 1. Introduction 1.1 Early Beginnings 1.2 The First Networks 1.3 Protocols as Languages 1.4 Protocol Standardization 1.5 Summary Exercises Bibliographic Notes 2. Protocol Structure 2.1 Introduction 2.2 The Five Elements of a Protocol 2.3 An Example 2.4 Service and Environment 2.5 Vocabulary and Format 2.6 Procedure Rules 2.7 Structured Protocol Design 2.8 Ten Rules of Design 2.9 Summary Exercises Bibliographic Notes 3. Error Control 3.1 Introduction 3.2 Error Model 3.3 Types of Transmission Errors 3.4 Redundancy 3.5 Types of Codes 3.6 Parity Check 3.7 Error Correction 3.8 A Linear Block Code 3.9 Cyclic Redundancy Checks CONTENTS ix xi 1 9 12 13 15 16 16 19 21 22 26 32 35 35 38 39 39 40 43 44 46 46 47 48 48 52 56 www.spinroot.com

3.10 Arithmetic Checksum 3.11 Summary Exercises Bibliographic Notes 4. Flow Control 4.1 Introduction 4.2 Window Protocols 4.3 Sequence Numbers 4.4 Negative Acknowledgments 4.5 Congestion Avoidance 4.6 Summary Exercises Bibliographic Notes Part II — Specification and Modeling 5. Validation Models 5.1 Introduction 5.2 Processes, Channels, Variables 5.3 Executability of Statements 5.4 Variables and Data Types 5.5 Process Types 5.6 Message Channels 5.7 Control Flow 5.8 Examples 5.9 Modeling Procedures and Recursion 5.10 Message Type Definitions 5.11 Modeling Timeouts 5.12 Lynch’s Protocol Revisited 5.13 Summary Exercises Bibliographic Notes 6. Correctness Requirements 6.1 Introduction 6.2 Reasoning about Behavior 6.3 Assertions 6.4 System Invariants 6.5 Deadlocks 6.6 Bad Cycles 6.7 Temporal Claims 6.8 Summary Exercises Bibliographic Notes 7. Protocol Design 7.1 Introduction 63 64 64 65 66 70 74 80 83 86 87 88 90 91 91 92 93 96 100 102 104 104 105 106 107 108 109 111 112 114 115 117 118 119 125 126 127 128 www.spinroot.com

7.2 Service Specification 7.3 Assumptions about the Channel 7.4 Protocol Vocabulary 7.5 Messsage Format 7.6 Procedure Rules 7.7 Summary Exercises Bibliographic Notes 8. Finite State Machines 8.1 Introduction 8.2 Informal Description 8.3 Formal Description 8.4 Execution of Machines 8.5 Minimization of Machines 8.6 The Conformance Testing Problem 8.7 Combining Machines 8.8 Extended Finite State Machines 8.9 Generalization of Machines 8.10 Restricted Models 8.11 Summary Exercises Bibliographic Notes Part III — Conformance Testing, Synthesis and Validation 9. Conformance Testing 9.1 Introduction 9.2 Functional Testing 9.3 Structural Testing 9.4 Deriving UIO Sequences 9.5 Modified Transition Tours 9.6 An Alternative Method 9.7 Summary Exercises Bibliographic Notes 10. Protocol Synthesis 10.1 Introduction 10.2 Protocol Derivation 10.3 Derivation Algorithm 10.4 Incremental Design 10.5 Place Synchronization 10.6 Summary Exercises Bibliographic Notes 11. Protocol Validation 129 130 131 133 140 160 160 161 162 162 169 170 171 174 175 176 178 181 184 185 185 187 188 189 195 196 197 199 200 200 203 203 208 210 210 211 212 212 www.spinroot.com

11.1 Introduction 11.2 Manual Proof Method 11.3 Automated Validation Methods 11.4 The Supertrace Algorithm 11.5 Detecting Non-Progress Cycles 11.6 Detecting Acceptance Cycles 11.7 Checking Temporal Claims 11.8 Complexity Management 11.9 Boundedness of PROMELA Models 11.10 Summary Exercises Bibliographic Notes Part IV — Design Tools 12. A Protocol Simulator 12.1 Introduction 12.2 SPIN — Overview 12.3 Expressions 12.4 Variables 12.5 Statements 12.6 Control Flow 12.7 Process and Message Types 12.8 Macro Expansion 12.9 SPIN Options 12.10 Summary Exercises Bibliographic Notes 13. A Protocol Validator 13.1 Introduction 13.2 Structure of the Validator 13.3 The Validation Kernel 13.4 The Transition Matrix 13.5 The Validator-Generator Code 13.6 Overview of the Code 13.7 Guided Simulation 13.8 Some Applications 13.9 Coverage in Supertrace Mode 13.10 Summary Exercises Bibliographic Notes 214 214 218 226 231 234 235 235 237 238 239 240 243 244 245 255 265 275 282 292 293 294 295 296 297 298 299 302 303 306 308 310 315 316 316 317 www.spinroot.com

14. Using the Validator 14.1 Introduction 14.2 An Optical Telegraph Protocol 14.3 Dekker’s Algorithm 14.4 A Larger Validation 14.5 Flow Control Validation 14.6 Session Layer Validation 14.7 Summary Exercises Bibliographic Notes Conclusion References Appendices Name Index Subject Index A. Data Transmission B. Flow Chart Language C. PROMELA Language Report D. SPIN Simulator Source E. SPIN Validator Source F. PROMELA File Transfer Protocol 318 318 320 322 325 336 349 349 349 351 352 367 380 383 393 436 528 537 539 www.spinroot.com

分享到：

赞收藏

资料库

Design and Validation of Computer Protocol.pdf

相关推荐

课程资源

热门标签

最新资料