This thesis addresses the problem of protocol verification. We first present a brief review of the existing specification methods for communication protocols, with emphasis on the hybrid techniques. The alternating bit protocol is specified in ISO/FDT, BBN/FST and UNISPEX to provide a comparison between three interesting hybrid models of protocol specification. A method for applying the unbounded state Temporal Logic to verify a protocol specified in a hybrid technique (in particular FDT) is outlined. Finally, a new specification and verification method called SETL is proposed, which is based on event sequences and temporal logic. To illustrate the method two data transfer protocols namely, the stop-wait and alternating bit protocols are specified in SETL and verified. We demonstrate that SETL is a generalization of the hybrid techniques, it is sound and that it can be semi-automated. / Science, Faculty of / Computer Science, Department of / Graduate

VALISYN, an automated system for the validation and synthesis of error-free protocols has been implemented in C language. It assists designers in the detection and prevention of various kinds of potential design errors, such as state deadlocks, non-executable interactions, unspecified receptions and state ambiguities. The technique employed is a stepwise application of a set of production rules which guarantee complete reception capability. These rules are implemented in a tracking algorithm, which prevents the formation of non-executable interactions and unspecified receptions, and which monitors the existence of state deadlocks and state ambiguities. The implementation of VALISYN is discussed and a number of protocol validation and synthesis examples are presented to illustrate its use and features. / Science, Faculty of / Computer Science, Department of / Graduate

No description available.

This thesis explores two strategies for supporting the development of network communication software: imposing constraints on protocol design at the specification level, and using a special-purpose language for protocol implementation. It presents a protocol implementation language called Morpheus. Morpheus utilizes the new strategies to provide a higher level of abstraction, finer grain modularity, and greater software reusability than previous approaches. Morpheus is able to provide a high level of abstraction because of built-in knowledge about its problem domain. It has a narrow problem domain--network protocols--that is further narrowed by the application of specification-level constraints. One particular constraint--the shapes constraint, which partitions protocols into three basic kinds--is particularly effective in raising the level of abstraction. Morpheus's support for modularity and, indirectly, software reuse hinges on reducing the performance penalty for layering. When protocol layering entails a high performance cost, developers are motivated to build complex monolithic implementations that are hard to design, implement, debug, modify, and maintain. Morpheus reduces the performance costs of layering by applying optimizations based on common patterns of protocol execution. If the degree of modularity is held fixed, then the optimizations simply improve performance. An optimization based on Integrated Layer Processing is particularly noteworthy for its dramatic contribution to network throughput while preserving modularity.

No description available.

No description available.

by Kong Tat Cheong. / Thesis (M.Sc.)--Chinese University of Hong Kong, 1992. / Includes bibliographical references (leaves 64-65). / Chapter CHAPTER 1. --- INTRODUCTION --- p.1 / Chapter CHAPTER 2. --- RECENT RESEARCH REVIEW --- p.4 / Chapter CHAPTER 3. --- IMAGE ACCESS PROTOCOL --- p.8 / Chapter 3.1 --- Design Principles --- p.11 / Chapter 3.2 --- Protocol Mechanism --- p.16 / Chapter 3.3 --- IAP Packet Formats --- p.20 / Chapter 3.4 --- Protocol Operation Example --- p.28 / Chapter CHAPTER 4. --- SYSTEM IMPLEMENTATION --- p.31 / Chapter 4.1 --- Software Architecture and Interfaces --- p.33 / Chapter 4.2 --- System Operations and Applications --- p.43 / Chapter 4.3 --- Image Transmission Efficiency --- p.48 / Chapter CHAPTER 5. --- ENHANCED SYSTEM SERVICES --- p.51 / Chapter 5.1 --- Progressive Coding --- p.51 / Chapter 5.2 --- Call Management --- p.56 / Chapter 5.3 --- Priority Control --- p.57 / Chapter 5.4 --- Concurrent Control --- p.58 / Chapter CHAPTER 6. --- CONCLUSION --- p.59 / Chapter APPENDIX 1. --- APPLICATION PROGRAMMING INTERFACE --- p.61 / REFERENCE --- p.64

Wen Yonggang. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2001. / Includes bibliographical references. / Abstracts in English and Chinese. / Chapter 1 --- Introduction / Chapter 1.1 --- Multi-Protocol Label Switching (MPLS) Technology --- p.1 / Chapter 1.2 --- Objective of this Thesis --- p.4 / Chapter 1.3 --- Reference --- p.5 / Chapter 2 --- Optical MPLS Network and Optical Label Schemes / Chapter 2.1 --- Optical MPLS Network --- p.7 / Chapter 2.2 --- Optical Label Schemes --- p.10 / Chapter 2.2.1 --- Time-division OMPLS scheme --- p.12 / Chapter 2.2.2 --- Wavelength-division OMPLS scheme --- p.16 / Chapter 2.2.3 --- Frequency-division OMPLS scheme --- p.22 / Chapter 2.2.3.1 --- UCSB Testbed --- p.23 / Chapter 2.2.3.2 --- UC-Davis Testbed --- p.26 / Chapter 2.2.3.3 --- NCTU-Telecordia Testbed --- p.28 / Chapter 2.2.4 --- Code-division OMPLS scheme --- p.30 / Chapter 2.2.4.1 --- Coherent Code-Division Label Scheme --- p.30 / Chapter 2.2.4.2 --- Noncoherent Code-Division Label Scheme --- p.32 / Chapter 2.3 --- Reference --- p.35 / Chapter 3 --- Architecture of OOC-based OMPLS network / Chapter 3.1 --- Infrastructure of OOC-label switch router (code converter) --- p.37 / Chapter 3.1.1 --- Architecture of the Proposed Code Converter --- p.38 / Chapter 3.1.2 --- Enhancement of the Code Converter --- p.41 / Chapter 3.2 --- Implementation of the OOC code converter --- p.43 / Chapter 3.2.1 --- Encoders/Decoders --- p.43 / Chapter 3.2.1.1 --- All-parallel encoders/decoders --- p.43 / Chapter 3.2.1.2 --- All-serial encoders/decoders --- p.45 / Chapter 3.2.1.3 --- Serial-to-parallel encoder/decoders --- p.47 / Chapter 3.2.1.4 --- Comparison of the three kinds of encoders/decoders --- p.49 / Chapter 3.2.2 --- Time-Gate-Intensity-Threshold (TGIT) Device --- p.50 / Chapter 3.2.3 --- Optical Space Switch Array --- p.54 / Chapter 3.2.3.1 --- All-optical Space Switch --- p.54 / Chapter 3.2.3.2 --- Optical switching technologies --- p.56 / Chapter 3.2.3.2.1 --- Scalability --- p.56 / Chapter 3.2.3.2.2 --- Switching Speed --- p.57 / Chapter 3.2.3.2.3 --- Reliability --- p.57 / Chapter 3.2.3.2.4 --- Losses --- p.58 / Chapter 3.2.3.2.5 --- Port-to-Port repeatability --- p.58 / Chapter 3.2.3.2.6 --- Cost --- p.59 / Chapter 3.2.3.2.7 --- Power Consumption --- p.60 / Chapter 3.3 --- Reference --- p.61 / Chapter 4 --- Scalability of OOC-based MPLS network / Chapter 4.1 --- Limitation on Label Switching Capacity --- p.63 / Chapter 4.1.1 --- Upper Bound --- p.65 / Chapter 4.1.2 --- Lower Bound --- p.66 / Chapter 4.2 --- Limitation on Switching Cascadability --- p.70 / Chapter 4.2.1. --- Limit Induced by the Inter-channel Crosstalk --- p.70 / Chapter 4.2.2 --- Limits Induced by the Residue Intensity of Sidelobes --- p.74 / Chapter 4.3 --- Appendix --- p.78 / Chapter 4.3.1 --- Derivation of Chip Intensity --- p.78 / Chapter 4.3.2 --- The 5% residue power criterion --- p.81 / Chapter 4.4 --- Reference --- p.83 / Chapter 5 --- Conclusion / Chapter 5.1 --- Summary of the Thesis --- p.85 / Chapter 5.2 --- Future work --- p.86

Liu Haiping. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2005. / Includes bibliographical references (leaves 78-82). / Abstracts in English and Chinese. / Acknowledgments --- p.i / Abstract --- p.ii / Table of Contents --- p.vi / List of Figures --- p.vii / List of Tables --- p.ix / Chapter Chapter I --- Introduction to Wireless LAN --- p.1 / Chapter 1.1 --- Wireless LAN Netwrok Architecture --- p.2 / Chapter 1.2 --- IEEE 802.11 protocol family --- p.4 / Chapter 1.3 --- The Major factors influencing the System Performance --- p.7 / Chapter 1.4 --- Research Objectives --- p.13 / Chapter 1.5 --- Overview --- p.13 / Chapter Chapter II --- The Major Deficiency of DCF and Motivation --- p.14 / Chapter 2.1 --- DCF --- p.15 / Chapter 2.2 --- The Major Deficiencies in the DCF --- p.20 / Chapter 2.3 --- Improvement directions --- p.24 / Chapter Chapter III --- Proposed MAC Protocol --- p.27 / Chapter 3.1 --- The Design Idea --- p.28 / Chapter 3.2 --- The Number of Active Nodes --- p.30 / Chapter 3.3 --- Optimizaition Method for CW --- p.32 / Chapter 3.4 --- CW and Counter value Updating --- p.35 / Chapter 3.5 --- Procedure Flow and Simulation Results --- p.37 / Chapter Chapter IV --- Advanced Proposed Protocol with QoS issues --- p.44 / Chapter 4.1 --- "QoS requirement, EDCF solution and others' work" --- p.45 / Chapter 4.2 --- Frame structure changes in the Advanced Proposed MAC Protocol --- p.47 / Chapter 4.3 --- Recursivley Balance Optimization Method for CW --- p.48 / Chapter 4.4 --- Decision Algorithm --- p.54 / Chapter 4.5 --- Model Validation and Simulation Results --- p.66 / Chapter Chapter V --- Further Discussion about CW design --- p.70 / Chapter 5.1 --- Influence of the ranges of CW --- p.71 / Chapter 5.2 --- Proposal for adjusting CW --- p.73 / Chapter Chapter VI --- Conclusion --- p.75 / Bibliography --- p.78

Thesis (Ph.D)--Stanford University, 2000. / Title from pdf t.p. (viewed Mar. 27, 2002). "May 2000." "Adminitrivia V1/Prg/20000602"--Metadata.