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

Multicasting can be done in two different ways: source based tree approach andshared tree approach. Shared tree approach is preferred over source-based treeapproach because in the later construction of minimum cost tree per source is neededunlike a single shared tree in the former approach. However, in shared tree approach asingle core needs to handle the entire traffic load resulting in degraded multicastperformance. Besides, it also suffers from „single point failure‟. Multicast is acommunication between one or multiple senders and multiple receivers, which used asa way of sending IP datagrams to a group of interested receivers in one transmission.Core-based trees major concerns are core selection and core as single point of failure.The problem of core selection is to choose the best core or cores in the network toimprove the network performance.In this dissertation we propose 1) a multiple core selection approach for core-based tree multicasting, senders can select different cores to have an efficient loadbalanced multicore multicasting. It will overcome any core failure as well. 2) Novel andefficient schemes for load shared multicore multicasting are presented. Multiple coresare selected statically, that is, independent of any existing multicast groups and also theselection process is independent of any underlying unicast protocol. Some of theselected cores can be used for fault- tolerant purpose also to guard against any possible core failures. 3) We have presented two novel and efficient schemes forgroup-based load shared multicore multicasting in which members of a multicast groupuse the same core tree for their multicasting. 4) We also presented two schemes aim atachieving low latency multicasting along with load sharing for delay sensitive multicastapplications. Besides, we have presented a unique approach for core migration, whichuses two very important parameters, namely, depth of a core tree and pseudo diameterof a core. One noteworthy point from the viewpoint of fault tolerance is that the degreeof fault-tolerance can be enhanced from covering single point-failure to any number ofcore failures.

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