Communication Protocol Engineering, Second Edition

The book aims to enable the reader to master the engineering of communication protocols, which are amply present nowadays in mobile phones, tablets, laptops, smart appliances, and service providers’ datacenters and clouds. Readers will acquire the theoretical knowledge and practical skills to successfully design, implement, test, and verify their solutions. The key benefits of the new edition align with the latest standard for conformance testing, TTCN-3, along with updated chapters. It explains process algebra CSP and how to model, simulate, and automatically verify CSP models in PAT. Cover 1 Half Title 2 Title Page 4 Copyright Page 5 Dedication 6 Table of Contents 8 Preface to the First Edition 14 Preface to the Second Edition 16 Author 18 Chapter 1: Introduction 20 1.1 The Notion of the Communication Protocol 24 References 27 Chapter 2: Requirements and Analysis 28 2.1 Use Case Diagrams 32 2.2 Collaboration Diagrams 40 2.3 Requirements and Analysis Example 50 2.3.1 SIP Domain Specifics 50 2.3.2 SIP Softphone Requirements Model 54 2.3.3 SIP Softphone Analysis Model 59 References 63 Chapter 3: Design 64 3.1 Class Diagrams 69 3.2 Object Diagrams 80 3.3 Sequence Diagrams 84 3.4 Activity Diagrams 92 3.5 Statechart Diagrams 108 3.6 Deployment Diagrams 121 3.7 Specification and Description Language 126 3.7.1 Telephone Call Processing Example 140 3.8 Message Sequence Charts 144 3.9 Tree and Tabular Combined Notation Version 3 148 3.9.1 TTCN-3 Language, Test Suite, and Test Systems 149 3.9.2 Basic TTCN-3 Constructs and Statements 157 3.9.3 Single Component TTCN-3 Test Suites 165 3.10 Examples 194 3.10.1 Example 1 194 3.10.2 Example 2 200 3.10.3 Example 3 207 3.10.4 Example 4 209 3.10.5 Example 5 217 References 226 Chapter 4: Implementation 228 4.1 Component Diagrams 230 4.2 Spectrum of FSM Implementations 236 4.3 State Design Pattern 256 4.4 Implementation Based on the FSM Library 260 4.4.1 Using the FSM Library 265 4.4.2 FSM Library Internals 267 4.4.2.1 FSMSystem Internals 268 4.4.2.2 FiniteStateMachine Internals 269 4.4.2.3 Kernel Internals 276 4.4.3 Writing FSM Library–Based Implementations 279 4.5 Examples 279 4.5.1 Example 1 280 4.5.2 Example 2 297 References 306 Chapter 5: Test and Verification 308 5.1 Unit Testing 312 5.2 Conformance Testing 322 5.3 Formal Verification 327 5.3.1 Formal Verification Based on Theorem Proving 327 5.3.2 Formal Verification Based on Communicating Sequential Processes 339 5.3.2.1 Brief Overview of CSP 339 5.3.2.2 Brief Overview of PAT and CSP# 343 5.3.2.2.1 CSP# Global Definitions 344 5.3.2.2.2 CSP# Process Definitions 346 5.3.2.2.3 CSP# Assertions 352 5.3.2.3 Examples of Formal Verification Based on CSP# and PAT 356 5.3.2.3.1 Alternating Bit Protocol 356 5.3.2.3.2 Two-Phase Commit Protocol 360 5.3.2.3.3 Leader Election in Complete Graphs 365 5.3.2.3.4 Leader Election in Rings 370 5.3.2.3.5 Leader Election in Trees 373 5.3.2.3.6 Telecomm Service System 375 5.4 Statistical Usage Testing 387 5.5 Examples 401 5.5.1 Example 1 402 5.5.2 Example 2 410 5.6 Further Reading 415 References 415 Chapter 6: FSM Library 418 6.1 Introduction 418 6.2 Basic FSM System Components 419 6.2.1 Class FSMSystem 419 6.2.1.1 FSM System Initialization 420 6.2.1.2 FSM System Startup 423 6.2.2 Class FiniteStateMachine 423 6.3 Time Management 426 6.4 Memory Management 427 6.5 Message Management 429 6.6 TCP/IP Support 433 6.6.1 Class FSMSystemWithTCP 434 6.6.2 Class NetFSM 435 6.7 Global Constants, Types, and Functions 437 6.8 API Functions 437 6.8.1 FSMSystem 450 6.8.2 Add(ptrFiniteStateMachine, uint8, uint32, bool) 451 6.8.3 Add(ptrFiniteStateMachine, uint8) 452 6.8.4 InitKernel 452 6.8.5 Remove(uint8) 453 6.8.6 Remove(uint8, uint32) 454 6.8.7 Start 454 6.8.8 StopSystem 454 6.8.9 FSMSystemWithTCP 455 6.8.10 InitTCPServer 455 6.8.11 FiniteStateMachine 456 6.8.12 AddParam 457 6.8.13 AddParamByte 458 6.8.14 AddParamDWord 458 6.8.15 AddParamWord 459 6.8.16 CheckBufferSize 459 6.8.17 ClearMessage 460 6.8.18 CopyMessage( ) 460 6.8.19 CopyMessage(uint*) 460 6.8.20 CopyMessageInfo 461 6.8.21 Discard 461 6.8.22 DoNothing 462 6.8.23 FreeFSM 462 6.8.24 GetAutomata 462 6.8.25 GetBitParamByteBasic 463 6.8.26 GetBitParamWordBasic 463 6.8.27 GetBitParamDWordBasic 464 6.8.28 GetBuffer 464 6.8.29 GetBufferLength 465 6.8.30 GetCallId 465 6.8.31 GetCount 466 6.8.32 GetGroup 466 6.8.33 GetInitialState 466 6.8.34 GetLeftMbx 467 6.8.35 GetLeftAutomata 467 6.8.36 GetLeftGroup 467 6.8.37 GetLeftObjectId 468 6.8.38 GetMbxId 468 6.8.39 GetMessageInterface 468 6.8.40 GetMsg() 469 6.8.41 GetMsg(uint8) 469 6.8.42 GetMsgCallId 470 6.8.43 GetMsgCode 470 6.8.44 GetMsgFromAutomata 470 6.8.45 GetMsgFromGroup 470 6.8.46 GetMsgInfoCoding 471 6.8.47 GetMsgInfoLength() 471 6.8.48 GetMsgInfoLength(uint8*) 471 6.8.49 GetMsgObjectNumberFrom 472 6.8.50 GetMsgObjectNumberTo 472 6.8.51 GetMsgToAutomata 472 6.8.52 GetMsgToGroup 473 6.8.53 GetNewMessage 473 6.8.54 GetNewMsgInfoCoding 473 6.8.55 GetNewMsgInfoLength 474 6.8.56 GetNextParam 474 6.8.57 GetNextParamByte 474 6.8.58 GetNextParamDWord 475 6.8.59 GetNextParamWord 476 6.8.60 GetObjectId 476 6.8.61 GetParam 477 6.8.62 GetParamByte 477 6.8.63 GetParamDWord 478 6.8.64 GetParamWord 479 6.8.65 GetProcedure 479 6.8.66 GetRightMbx 480 6.8.67 GetRightAutomata 480 6.8.68 GetRightGroup 480 6.8.69 GetRightObjectId 481 6.8.70 GetState 481 6.8.71 IsBufferSmall 481 6.8.72 Initialize 482 6.8.73 InitEventProc 482 6.8.74 InitTimerBlock 483 6.8.75 InitUnexpectedEventProc 483 6.8.76 IsTimerRunning 484 6.8.77 NoFreeObjectProcedure 484 6.8.78 NoFreeInstances 485 6.8.79 ParseMessage 485 6.8.80 PrepareNewMessage(uint8*) 486 6.8.81 PrepareNewMessage(uint32, uint16, uint8) 486 6.8.82 Process 487 6.8.83 PurgeMailBox 487 6.8.84 RemoveParam 488 6.8.85 Reset 488 6.8.86 ResetTimer 488 6.8.87 RestartTimer 489 6.8.88 RetBuffer 489 6.8.89 ReturnMsg 489 6.8.90 SetBitParamByteBasic 490 6.8.91 SetBitParamDWordBasic 490 6.8.92 SetBitParamWordBasic 491 6.8.93 SetCallId() 491 6.8.94 SetCallId(uint32) 491 6.8.95 SetCallIdFromMsg 492 6.8.96 SetDefaultFSMData 492 6.8.97 SetDefaultHeader 492 6.8.98 SetGroup 493 6.8.99 SetInitialState 493 6.8.100 SetKernelObjects 493 6.8.101 SetLeftMbx 494 6.8.102 SetLeftAutomata 494 6.8.103 SetLeftObject 494 6.8.104 SetLeftObjectId 495 6.8.105 SetLogInterface 495 6.8.106 SendMessage(uint8) 495 6.8.107 SendMessage(uint8, uint8*) 496 6.8.108 SetMessageFromData 496 6.8.109 SetMsgCallId(uint32) 496 6.8.110 SetMsgCallId(unit32, unit8*) 497 6.8.111 SetMsgCode(uint16) 497 6.8.112 SetMsgCode(uint16, uint8*) 497 6.8.113 SetMsgFromAutomata(uint8) 498 6.8.114 SetMsgFromAutomata(uint8, uint8*) 498 6.8.115 SetMsgFromGroup(uint8) 498 6.8.116 SetMsgFromGroup(uint8, uint8*) 499 6.8.117 SetMsgInfoCoding(uint8) 499 6.8.118 SetMsgInfoCoding(uint8, uint8*) 500 6.8.119 SetMsgInfoLength(uint16) 500 6.8.120 SetMsgInfoLength(uint16, uint8*) 500 6.8.121 SetMsgObjectNumberFrom(uint32) 501 6.8.122 SetMsgObjectNumberFrom(uint32, uint8*) 501 6.8.123 SetMsgObjectNumberTo(uint32) 501 6.8.124 SetMsgObjectNumberTo(uint32, uint8*) 502 6.8.125 SetMsgToAutomata(uint8) 502 6.8.126 SetMsgToAutomata(uint8, uint8*) 502 6.8.127 SetMsgToGroup(uint8) 503 6.8.128 SetMsgToGroup(uint8, uint8*) 503 6.8.129 SendMessageLeft 503 6.8.130 SendMessageRight 504 6.8.131 SetNewMessage 504 6.8.132 SetObjectId 504 6.8.133 SetRightMbx 505 6.8.134 SetRightAutomata 505 6.8.135 SetRightObject 505 6.8.136 SetRightObjectId 506 6.8.137 SetState 506 6.8.138 StartTimer 506 6.8.139 StopTimer 506 6.8.140 SysClearLogFlag 507 6.8.141 SysStartAll 507 6.8.142 NetFSM 507 6.8.143 convertFSMToNetMessage 508 6.8.144 convertNetToFSMMessage 508 6.8.145 establishConnection 509 6.8.146 getProtocolInfoCoding 509 6.8.147 sendToTCP 509 6.9 A Simple Example with Three Automata Instances 509 6.10 A Simple Example with Network-Aware Automata Instances 538 Index 556 Content: Chapter 1 Introduction1.1 The Notion of the Communication ProtocolReferencesChapter 2 Requirements and Analysis2.1 Use Case Diagrams2.2 Collaboration Diagrams2.3 Requirements and Analysis ExampleReferencesChapter 3 Design3.1 Class Diagrams3.2 Object Diagrams3.3 Sequence Diagrams3.4 Activity Diagrams3.5 Statechart Diagrams3.6 Deployment Diagrams3.7 Specification and Description Language3.8 Message Sequence Charts3.9 Tree and Tabular Combined Notation3.10 ExamplesReferencesChapter 4 Implementation4.1 Component Diagrams4.2 The Spectrum of FSM Implementations4.3 State Design Pattern4.4 Implementation Based on the FSM Library4.5 ExamplesReferencesChapter 5 Test and Verification5.1 Unit Testing5.2 Conformance Testing5.3 Formal Verification Based on Theorem Proving5.4 Statistical Usage Testing5.5 Examples5.6 Further ReadingReferencesChapter 6 FSM Library6.1 Introduction6.2 Basic FSM System Components6.3 Time Management6.4 Memory Management6.5 Message Management6.6 TCP/IP Support6.7 Global Constants, Types, and Functions6.8 API Functions6.9 A Simple Example with Three Automata Instances6.10 A Simple Example with Network-Aware Automata Instances