text: In this paper, we present a new methodology for developing systematic and automatic test generation algorithms for multipoint protocols. These algorithms attempt to synthesize network topologies and sequences of events that stress the protocol's correctness or performance. This problem can be viewed as a domain-specific search problem that suffers from the state space explosion problem. One goal of this work is to circumvent the state space explosion problem utilizing knowledge of network and fault modeling, and multipoint protocols. The two approaches investigated in this study are based on forward and backward search techniques. We use an extended finite state machine (FSM) model of the protocol. The first algorithm uses forward search to perform reduced reachability analysis. Using domain-specific information for multicast routing over LANs, the algorithm complexity is reduced from exponential to polynomial in the number of routers. This approach, however, does not fully automate topology synthesis. The second algorithm, the fault-oriented test generation, uses backward search for topology synthesis and uses backtracking to generate event sequences instead of searching forward from initial states. Using these algorithms, we have conducted studies for correctness of the multicast routing protocol PIM. We propose to extend these algorithms to study end-to-end multipoint protocols using a virtual LAN that represents delays of the underlying multicast distribution tree.
  @cite_13: In order for the nodes of a distributed computer network to communicate, each node must have information about the network's topology. Since nodes and links sometimes crash, a scheme is needed to update this information. One of the major constraints on such a topology information scheme is that it may not involve a central controller. The Topology Information Protocol that was implemented on the MERIT Computer Network is presented and explained; this protocol is quite general and could be implemented on any computer network. It is based on Baran's “Hot Potato Heuristic Routing Doctrine.” A correctness proof of this Topology Information Protocol is also presented.
  @cite_38: Aho, Ullman, and Yannakakis have proposed a set of protocols that ensure reliable transmission of data across an error-prone channel. They have obtained lower bounds on the complexity required of the protocols to assure reliability for different classes of errors. They specify these protocols with finite-state machines. Although the protocol machines have only a small number of states, they are nontrivial to prove correct. In this paper we present proofs of one of these protocols using the finite-state-machine approach and the abstract-program approach. We also show that the abstract-program approach gives special insight into the operation of the protocol.
  @cite_22: A new distributed algorithm is presented for dynamically determining weighted shortest paths used for message routing in computer networks. The major features of the algorithm are that the paths defined do not form transient loops when weights change and the number of steps required to find new shortest paths when network links fail is less than for previous algorithms. Specifically, the worst case recovery time is proportional to the largest number of hops h in any of the weighted shortest paths. For previous loop-free distributed algorithms this recovery time is proportional to h2.
  @cite_42: My goal is to propose a set of questions that I think are important. J. Misra and I are working on these questions.
  @cite_39: 
  @cite_44: 
  @cite_24: An algorithm for constructing and adaptively maintaining routing tables in communication networks is presented. The algorithm can be employed in message as well as circuit switching networks, uses distributed computation, provides routing tables that are loop-free for each destination at all times, adapts to changes in network flows, and is completely failsafe. The latter means that after arbitrary failures and additions, the network recovers in finite time in the sense of providing routing paths between all physically connected nodes. For each destination, the routes are independently updated by an update cycle triggered by the destination.
  @cite_40: Mobile computing represents a major point of departure from the traditional distributed computing paradigm. The potentially very large number of independent computing units, a decoupled computing style, frequent disconnections, continuous position changes, and the location-dependent nature of the behavior and communication patterns of the individual components present designers with unprecedented challenges in the areas of modularity and dependability. The paper describes two ideas regarding a modular approach to specifying and reasoning about mobile computing. The novelty of our approach rests with the notion of allowing transient interactions among programs which move in space. We restrict our concern to pairwise interactions involving variable sharing and action synchronization. The motivation behind the transient nature of the interactions comes from the fact that components can communicate with each other only when they are within a certain range. The notation we propose is meant to simplify the writing of mobile applications and is a direct extension of that used in UNITY. Reasoning about mobile computations relies on the UNITY proof logic.
  @cite_19: 
  @cite_10: This paper deals with a distributed adaptive routing strategy which is very simple and effective, and is free of a ping-pong-type looping in the presence of network failures. Using the number of time intervals required for a node to recover from a network failure as the measure of network's adaptability, performance of this strategy and the ARPANET's previous routing strategy (APRS) is comparatively analyzed without resorting to simulation. Formulas of the exact number of time intervals required for failure recovery under both strategies are also derived. We show that i)the performance of the strategy is always better than, or at least as good as, that of APRS, and ii) network topology has significant effects on the performance of both strategies.
  @cite_20: 0. Introduction.- 1. Experimenting on nondeterministic machines.- 2. Synchronization.- 3. A case study in synchronization and proof techniques.- 4. Case studies in value-communication.- 5. Syntax and semantics of CCS.- 6. Communication trees (CTs) as a model of CCS.- 7. Observation equivalence and its properties.- 8. Some proofs about data structures.- 9. Translation into CCS.- 10. Determinancy and confluence.- 11. Conclusion.
summary: Several attempts to apply formal verification to network protocols have been made. Assertional proof techniques were used to prove distance vector routing @cite_13 , path vector routing @cite_10 and route diffusion algorithms @cite_22 @cite_44 and @cite_24 using communicating finite state machines. An example point-to-point mobile application was proved using assertional reasoning in @cite_40 using UNITY @cite_42 . Axiomatic reasoning was used in proving a simple transmission protocol in @cite_38 . Algebraic systems based on the calculus of communicating systems (CCS) @cite_20 have been used to prove CSMA CD @cite_19 . Formal verification has been applied to TCP and T TCP in @cite_39 .