{'fraction_non_alphanumeric': 0.032319354776168596, 'fraction_numerical': 0.004420403652649334, 'mean_word_length': 4.701967720539465, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Systematic Testing of Multicast Routing Protocols: Analysis of Forward and Backward Search Techniques

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.


I. Introduction
Network protocols are becoming more complex with the exponential growth of the Internet, and the introduction of new services at the network, transport and application levels. In particular, the advent of IP multicast and the MBone enabled applications ranging from multi-player games to distance learning and teleconferencing, among others. To date, little effort has been exerted to formulate systematic methods and tools that aid in the design and characterization of these protocols.
In addition, researchers are observing new and obscure, yet all too frequent, failure modes over the internets [1] [2]. Such failures are becoming more frequent, mainly due to the increased heterogeneity of technologies, interconnects and configuration of various network components. Due to the synergy and interaction between different network protocols and components, errors at one layer may lead to failures at other layers of the protocol stack. Furthermore, degraded performance of low level network protocols may have ripple effects on end-to-end protocols and applications.
Network protocol errors are often detected by application failure or performance degradation. Such errors are hardest to diagnose when the behavior is unexpected or unfamiliar. Even if a protocol is proven to be correct in isolation, its behavior may be unpredictable in an operational network, where interaction with other protocols and the presence of failures may affect its operation. Protocol errors may be very costly to repair if discovered after deployment. Hence, endeavors should be made to capture protocol flaws early in the design cycle before deployment. To provide an effective solution to the above problems, we present a framework for the systematic design and testing of multicast protocols. The framework integrates test generation algorithms with simulation and implementation. We propose a suite of practical methods and tools for automatic test generation for network protocols.
Many researchers [3] [4] have developed protocol verification methods to ensure certain properties of protocols, like freedom from deadlocks or unspecified receptions. Much of this work, however, was based on assumptions about the network conditions, that may not always hold in today's Internet, and hence may become invalid. Other approaches, such as reachability analysis, attempt to check the protocol state space, and generally suffer from the 'state explosion' problem. This problem is exacerbated with the increased complexity of the protocol. Much of the previous work on protocol verification targets correctness. We target protocol performance and robustness in the presence of network failures. In addition, we provide new methods for studying multicast protocols and topology synthesis that previous works do not provide.
We investigate two approaches for test generation. The first approach, called the fault-independent test generation, uses a forward search algorithm to explore a subset of the protocol state space to generate the test events automatically. State and fault equivalence relations are used in this approach to reduce the state space. The second approach is called the fault-oriented test generation, and uses a mix of forward and backward search techniques to synthesize test events and topologies automatically.
We have applied these methods to multicast routing. Our case studies revealed several design errors, for which we have formulated solutions with the aid of this systematic process.
We further suggest an extension of the model to include end-to-end delays using the notion of virtual LAN. Such extension, in conjunction with the fault-oriented test generation, can be used for performance evaluation of end-to-end multipoint protocols.
The rest of this document is organized as follows. Sec-tion VI presents related work in protocol verification, conformance testing and VLSI chip testing. Section II introduces the proposed framework, and system definition. Sections III, IV, V present the search based approaches and problem complexity, the fault-independent test generation and the fault-oriented test generation, respectively. Section VII concludes 1 .
• Multicast Routing Overview Multicast protocols are the class of protocols that support group communication. Multicast routing protocols include, DVMRP [5], MOSPF [6], PIM-DM [7], CBT [8], and PIM-SM [9]. Multicast routing aims to deliver packets efficiently to group members by establishing distribution trees. Figure 1 shows a very simple example of a source S sending to a group of receivers Ri. Multicast distribution trees may be established by either broadcast-and-prune or explicit join protocols. In the former, such as DVMRP or PIM-DM, a multicast packet is broadcast to all leaf subnetworks. Subnetworks with no local members for the group send prune messages towards the source(s) of the packets to stop further broadcasts. Link state protocols, such as MOSPF, broadcast membership information to all nodes. In contrast, in explicit join protocols, such as CBT or PIM-SM, routers send hop-by-hop join messages for the groups and sources for which they have local members. We conduct robustness case studies for PIM-DM. We are particularly interested in multicast routing protocols, because they are vulnerable to failure modes, such as selective loss, that have not been traditionally studied in the area of protocol design. For most multicast protocols, when routers are connected via a multi-access network (or LAN) 2 , hop-by-hop messages are multicast on the LAN, and may experience selective loss; i.e. may be received by some nodes but not others. The likelihood of selective loss is increased by the fact that LANs often 1 We include appendices for completeness. 2 We use the term LAN to designate a connected network with respect to IP-multicast. This includes shared media (such as Ethernet, or FDDI), hubs, switches, etc. contain hubs, bridges, switches, and other network devices. Selective loss may affect protocol robustness. Similarly, end-to-end multicast protocols and applications must deal with situations of selective loss. This differentiates these applications most clearly from their unicast counterparts, and raises interesting robustness questions. Our case studies illustrate why selective loss should be considered when evaluating protocol robustness. This lesson is likely to extend to the design of higher layer protocols that operate on top of multicast and can have similar selective loss.

II. Framework Overview
Protocols may be evaluated for correctness or performance. We refer to correctness studies that are conducted in the absence of network failures as verification. In contrast, robustness studies consider the presence of network failures (such as packet loss or crashes). In general, the robustness of a protocol is its ability to respond correctly in the face of network component failures and packet loss. This work presents a methodology for studying and evaluating multicast protocols, specifically addressing robustness and performance issues. We propose a framework that integrates automatic test generation as a basic component for protocol design, along with protocol modeling, simulation and implementation testing. The major contribution of this work lies in developing new methods for generating stress test scenarios that target robustness and correctness violation, or worst case performance.
Instead of studying protocol behavior in isolation, we incorporate the protocol model with network dynamics and failures in order to reveal more realistic behavior of protocols in operation.
This section presents an overview of the framework and its constituent components. The model used to represent the protocol and the system is presented along with definitions of the terms used.
Our framework integrates test generation with simulation and implementation code. It is used for Systematic Testing of Robustness by Evaluation of Synthesized Scenarios (STRESS). As the name implies, systematic methods for scenario synthesis are a core part of the framework. We use the term scenarios to denote the test-suite consisting of the topology and events.
The input to this framework is the specification of a protocol, and a definition of its design requirements, in terms of correctness or performance. Usually robustness is defined in terms of network dynamics or fault models. A fault model represents various component faults; such as packet loss, corruption, re-ordering, or machine crashes. The desired output is a set of test-suites that stress the protocol mechanisms according to the robustness criteria.
As shown in Figure 2, the STRESS framework includes test generation, detailed simulation driven by the synthesized tests, and protocol implementation driven through an emulation interface to the simulator. In this work we focus on the test generation (TG) component. The STRESS framework

A. Test Generation
The core contribution of our work lies in the development of systematic test generation algorithms for protocol robustness. We investigate two such algorithms, each using a different approach.
In general test generation may be random or deterministic. Generation of random tests is simple but a large set of tests is needed to achieve a high measure of error coverage. Deterministic test generation (TG), on the other hand, produces tests based on a model of the protocol. The knowledge built into the protocol model enables the production of shorter and higher-quality test sequences. Deterministic TG can be: a) fault-independent, or b) fault-oriented. Fault-independent TG works without targeting individual faults as defined by the fault model. Such an approach may employ a forward search technique to inspect the protocol state space (or an equivalent subset thereof), after integrating the fault into the protocol model. In this sense, it may be considered a variant of reachability analysis. We use the notion of equivalence to reduce the search complexity. Section IV describes our fault-independent approach.
In contrast, fault-oriented tests are generated for specified faults. Fault-oriented test generation starts from the fault (e.g. a lost message) and synthesizes the necessary topology and sequence of events that trigger the error. This algorithm uses a mix of forward and backward searches. We present our fault-oriented algorithm in Section V.
We conduct case studies for the multicast routing protocol PIM-DM to illustrate differences between the approaches, and provide a basis for comparison.
In the remainder of this section, we describe the system model and definition.

B. The system model
We define our target system in terms of network and topology elements and a fault model.

B.1 Elements of the network
Elements of the network consist of multicast capable nodes and bi-directional symmetric links. Nodes run same multicast routing, but not necessarily the same unicast routing. The topology is an N -router LAN modeled at the network level; we do not model the MAC layer.
For end-to-end performance evaluation, the multicast distribution tree is abstracted out as delays between end systems and patterns of loss for the multicast messages. Cascade of LANs or uniform topologies are addressed in future research.

B.2 The fault model
We distinguish between the terms error and fault. An error is a failure of the protocol as defined in the protocol design requirement and specification. For example, duplication in packet delivery is an error for multicast routing. A fault is a low level (e.g. physical layer) anomalous behavior, that may affect the behavior of the protocol under test. Note that a fault may not necessarily be an error for the low level protocol.
The fault model may include: (a) Loss of packets, such as packet loss due to congestion or link failures. We take into consideration selective packet loss, where a multicast packet may be received by some members of the group but not others, (b) Loss of state, such as multicast and/or unicast routing tables, due to machine crashes or insufficient memory resources, (c) The delay model, such as transmission, propagation, or queuing delays. For end-to-end multicast protocols, the delays are those of the multicast distribution tree and depend upon the multicast routing protocol, and (d) Unicast routing anomalies, such as route inconsistencies, oscillations or flapping.
Usually, a fault model is defined in conjunction with the robustness criteria for the protocol under study. For our robustness studies we study PIM. The designing robustness goal for PIM is to be able to recover gracefully (i.e. without going into erroneous stable states) from single protocol message loss. That is, being robust to a single message loss implies that transitions cause the protocol to move from one correct stable state to another, even in the presence of selective message loss. In addition, we study PIM protocol behavior in presence of crashes and route inconsistencies.

C. Test Sequence Definition
A fault model may include a single fault or multiple faults. For our robustness studies we adopt a single-fault model, where only a single fault may occur during a scenario or a test sequence.
We define two sequences, T =< e1, e2, . . . , en > and T ′ =< e1, e2, . . . , ej, f, e k , . . . , en >, where ei is an event and f is a fault. Let P (q, T ) be the sequence of states and stimuli of protocol P under test T starting from the initial state q. T ′ is a test sequence if final P (q, T ′ ) is incorrect; i.e. the stable state reached after the occurrence of the fault does not satisfy the protocol correctness conditions (see Section II-E) irrespective of P (q, T ). In case of a fault-free sequence, where T = T ′ , the error is attributed to a protocol design error. Whereas when T = T ′ , and final P (q, T ) is correct, the error is manifested by the fault. This definition ignores transient protocol behavior. We are only concerned with the stable (i.e. non-transient) behavior of a protocol.

D. Test Scenario
A test scenario is defined by a sequence of (host) events, a topology, and a fault model, as shown in Figure 3. The events are actions performed by the host and act as input to the system; for example, join, leave, or send packet. The topology is the routed topology of set of nodes and links. The nodes run the set of protocols under test or other supporting protocols. The links can be either point-to-point links or LANs. This model may be extended later to represent various delays and bandwidths between pairs of nodes, by using a virtual LAN matrix (see [10]). The fault model used to inject the fault into the test. According to our singlemessage loss model, for example, a fault may denote the 'loss of the second message of type prune traversing a certain link'. Knowing the location and the triggering action of the fault is important in analyzing the protocol behavior.

E. Brief description of PIM-DM
For our robustness studies, we apply our automatic test generation algorithms to a version of the Protocol Independent Multicast-Dense Mode, or PIM-DM. The description given here is useful for Sections III through V.
PIM-DM uses broadcast-and-prune to establish the multicast distribution trees. In this mode of operation, a multicast packet is broadcast to all leaf subnetworks. Subnetworks with no local members send prune messages towards the source(s) of the packets to stop further broadcasts.
Routers with new members joining the group trigger Graft messages towards previously pruned sources to re-establish the branches of the delivery tree. Graft messages are acknowledged explicitly at each hop using the Graft-Ack message.
PIM-DM uses the underlying unicast routing tables to get the next-hop information needed for the RPF (reverse-pathforwarding) checks. This may lead to situations where there are multiple forwarders for a LAN. The Assert mechanism prevents these situations and ensures there is at most one forwarder for a LAN.
The correct function of a multicast routing protocol in general, is to deliver data from senders to group members (only those that have joined the group) without any data loss. For our methods, we only assume that a correctness definition is given by the protocol designer or specification. For illustration, we discuss the protocol errors and the correctness conditions.

E.1 PIM Protocol Errors
In this study we target protocol design and specification errors. We are interested mainly in erroneous stable (i.e. non-transient) states. In general, the protocol errors may be defined in terms of the end-to-end behavior as functional correctness requirements. In our case, for PIM-DM, an error may manifest itself in one of the following ways: 1) black holes: consecutive packet loss between periods of packet delivery, 2) packet looping: the same packet traverses the same set of links multiple times, 3) packet duplication: multiple copies of the same packet are received by the same receiver(s), 4) join latency: lack of packet delivery after a receiver joins the group, 5) leave latency: unnecessary packet delivery after a receiver leaves the group 3 , and 6) wasted bandwidth: unnecessary packet delivery to network links that do not lead to group members.

E.2 Correctness Conditions
We assume that correctness conditions are provided by the protocol designer or the protocol specification. These conditions are necessary to avoid the above protocol errors in a LAN environment, and include 4 : 1. If one (or more) of the routers is expecting to receive packets from the LAN, then one other router must be a forwarder for the LAN. Violation of this condition may lead to data loss (e.g. join latency or black holes). 2. The LAN must have at most one forwarder at a time. Violation of this condition may lead to data packet duplication. 3. The delivery tree must be loop-free: (a) Any router should accept packets from one incoming interface only for each routing entry. This condition is enforced by the RPF (Reverse Path Forwarding) check.
(b) The underlying unicast topology should be loop-free 5 . Violation of this condition may lead to data packet looping. 4. If one of the routers is a forwarder for the LAN, then there must be at least one router expecting packets from the LANs. Violation of this condition may lead to leave latency.

III. Search-based Approaches
The problem of test synthesis can be viewed as a search problem. By searching the possible sequences of events and 3 Join and leave latencies may be considered in other contexts as performance issues. However, in our study we treat them as errors. 4 These are the correctness conditions for stable states; i.e. not during transients, and are defined in terms of protocol states (as opposed to end point behavior). The mapping from functional correctness requirements for multicast routing to the definition in terms of the protocol model is currently done by the designer. The automation of this process is part of future research. 5 Some esoteric scenarios of route flapping may lead to multicast loops, in spite of RPF checks. Currently, our study does not address this issue, as it does not pertain to a localized behavior.
faults over network topologies and checking for design requirements (either correctness or performance), we can construct the test scenarios that stress the protocol. However, due to the state space explosion, techniques must be used to reduce the complexity of the space to be searched. We attempt to use these techniques to achieve high test quality and protocol coverage. Following we present the GFSM model for the case study protocol (PIM-DM), and use it as an illustrative example to analyze the complexity of the state space and the search problem, as well as illustrate the algorithmic details and principles involved in FITG and FOTG.

A. The Protocol Model
We represent the protocol as a finite state machine (FSM) and the overall LAN system by a global FSM (GFSM). I. FSM model: Every instance of the protocol, running on a single router, is modeled by a deterministic FSM consisting of: (i) a set of states, (ii) a set of stimuli causing state transitions, and (iii) a state transition function (or table) describing the state transition rules. For a system i, this is represented by the machine Mi = (S, τi, δi), where S is a finite set of state symbols, τi is the set of stimuli, and δi is the state transition function S × τi → S.
II. Global FSM model: The global state is defined as the composition of individual router states. The output messages from one router may become input messages to other routers. Such interaction is captured by the GFSM model in the global transition table. The behavior of a system with n routers may be described by MG = (SG, τG, δG), where SG: S1 × S2 × · · · × Sn is the global state space, τG: τi is the set of stimuli, and δG is the global state transition function SG × τG → SG.
The fault model is integrated into the GFSM model. For message loss, the transition caused by the message is either nullified or modified, depending on the selective loss pattern. Crashes may be treated as stimuli causing the routers affected by the crash to transit into a crashed state 6 . Network delays are modeled (when needed) through the delay matrix presented in Section VII. For a given group and a given source (i.e., for a specific source-group pair), we define the states w.r.t. a specific LAN to which the router Ri is attached. For example, a state may indicate that a router is a forwarder for (or a receiver expecting packets from) the LAN. 6 The crashed state maybe one of the states already defined for the protocol, like the empty state, or may be a new state that was not defined previously for the protocol. The possible states for upstream and downstream routers are as follows:

B. PIM-DM Model
if the router is upstream; if the router is downstream.
The stimuli considered here include transmitting and receiving protocol messages, timer events, and external host events. Only stimuli leading to change of state are considered. For example, transmitting messages per se (vs. receiving messages) does not cause any change of state, except for the Graf t, in which case the Rtx timer is set. Following are the stimuli considered in our study: 1. Transmitting messages: Graft transmission (Graf tT x). 2. Receiving messages: Graft reception (Graf tRcv), Join reception (Join), Prune reception (P rune), Graft Acknowledgement reception (GAck), Assert reception (Assert), and forwarded packets reception (F P kt).
3. Timer events: these events occur due to timer expiration (Exp) and include the Graft re-transmission timer (Rtx), the event of its expiration (RtxExp), the forwarder-deletion timer (Del), and the event of its expiration (DelExp). We refer to the event of timer expiration as (T imerImplication).

B.2 Global FSM model
Subscripts are added to distinguish different routers. These subscripts are used to describe router semantics and how routers interact on a LAN. An example global state for a topology of 4 routers connected to a LAN, with router 1 as a forwarder, router 2 expecting packets from the LAN, and routers 3 and 4 have negative caches, is given by {F1, N H2, N C3, N C4}. For the global stimuli τG, subscripts are added to stimuli to denote their originators and recipients (if any). The global transition rules δG are extended to encompass the router and stimuli subscripts 7 .
7 Semantics of the global stimuli and global transitions will be described as needed (see Section V).

C. Defining stable states
We are concerned with stable state (i.e. non-transient) behavior, defined in this section. To obtain erroneous stable states, we need to define the transition mechanisms between such states. We introduce the concept of transition classification and completion to distinguish between transient and stable states.

C.1 Classification of Transitions
We identify two types of transitions; externally triggered (ET) and internally triggered (IT) transitions. The former is stimulated by events external to the system (e.g., HJoin or Leave), whereas the latter is stimulated by events internal to the system (e.g., F P kt or Graf t).
We note that some transitions may be triggered due to either internal and external events, depending on the scenario. For example, a P rune may be triggered due to forwarding packets by an upstream router F P kt (which is an internal event), or a Leave (which is an external event).
A global state is checked for correctness at the end of an externally triggered transition after completing its dependent internally triggered transitions.
Following is a or Leave). Therefore, we should be able to identify a transition based upon its stimuli (either external or internal).
At the end of each complete transition sequence the system exists in either a correct or erroneous stable state. Eventtriggered timers (e.g., Del, Rtx) fire at the end of a complete transition.

D. Problem Complexity
The problem of finding test scenarios leading to protocol error can be viewed as a search problem of the protocol state space. Conventional reachability analysis [11] attempts to investigate this space exhaustively and incurs the 'state space explosion' problem. To circumvent this problem we use search reduction techniques using domain-specific information of multicast routing.
In this section, we give the complexity of exhaustive search, then discuss the reduction techniques we employ based on notion of equivalence, and give the complexity of the state space.

D.1 Complexity of exhaustive search
Exhaustive search attempts to generate all states reachable from initial system states. In the symbolic representation, r routers in state q are represented by q r . The global state for a system of n routers 8 Crashes force any state to the empty state. 9 Two system states (q 1 , q 2 , . . . , qn) and (p 1 , p 2 , . . . , pn) are strictly However, all routers use the same deterministic FSM model, hence all n! permutations of (q 1 , q 2 , . . . , qn) are equivalent. A global state for a system with n routers may be represented as 10 The notion of counting equivalence also applies to transitions and faults.
Those transitions or faults leading to equivalent states are considered equivalent.
To satisfy the correctness conditions for PIM-DM, the correct stable global states are those containing no forwarders and no routers expecting packets, or those containing one forwarder and one or more routers expecting packets from the link; symbolically this may be given by: We use X to denote any state si ∈ S. The correct space and the erroneous space must be disjoint and they must be complete (i.e. add up to the complete space), otherwise the specification is incorrect. See Appendix I-A for details.
We present two correctness definitions that are used in our case.
• The first definition considers the forwarder states as F and the routers expecting packets from the LAN as N H. Hence, the symbolic representation of the correct states becomes: 11 For convenience, we may represent these two states as G 1 = NC * , and G 2 = F, NH 1+ , NC * . 12 These conditions we have found to be reasonably sufficient to meet the functional correctness requirements. However, they may not be necessary, hence the search may generate false errors. Proving necessity is part of future work. and the number of correct states is: • The second definition considers the forwarder states as {Fi, F i Del } or simply FX , and the states expecting packets from the LAN as {N Hi, N Hi Rtx} or simply N HX . Hence, the symbolic representation of the correct states becomes: and the number of correct states is: Refer to Appendix I-B for more details on deriving the number of correct states.
In general, we find that the size of the error state space, according to both definitions, constitutes the major portion of the whole state space. This means that search techniques explicitly exploring the error states are likely to be more complex than others. We take this in consideration when designing our methods.

IV. Fault-independent Test Generation
Fault-independent test generation (FITG) uses the forward search technique to investigate parts of the state space. As in reachability analysis, forward search starts from initial states and applies the stimuli repeatedly to produce the reachable state space (or part thereof). Conventionally, an exhaustive search is conducted to explore the state space. In the exhaustive approach all reachable states are expanded until the reachable state space is exhausted. We use several manifestations of the notion of counting equivalence introduced earlier to reduce the complexity of the exhaustive algorithm and expand only equivalent subspaces. To examine robustness of the protocol, we incorporate selective loss scenarios into the search.

A. Reduction Using Equivalences
The search procedure starts from the initial states 13 and keeps a list of states visited to prevent looping. Each state is expanded by applying the stimuli and advancing the state machine forward by implementing the transition rules and returning a new stable state each time 14 . We use the counting equivalence notion to reduce the complexity of the search in three stages of the search: 1. The first reduction we use is to investigate only the equivalent initial states. To achieve this we simply treat the set of states constituting the global state as unordered set 13 For our case study the routers start as either a non-member (NM ) or empty upstream routers (EU ), that is, the initial states I.S. = {NM, EU }.
14 For details of the above procedures, see Appendix II-A. One procedure that produces such equivalent initial state space given in Appendix II-B. The complexity of the this algorithm is given by C(n + i.s. − 1, n) as was shown in Section III-D.2 and verified through simulation.

B. Applying the Method
In this section we discuss how the fault-independent test generation can be applied to the model of PIM-DM. We apply forward search techniques to study correctness of PIM-DM. We first study the complexity of the algorithms without faults. Then we apply selective message loss to study the protocol behavior and analyze the protocol errors.
More detailed presentation of the algorithmic details and results are given in Appendix II.
For robustness analysis (vs. verification), faults are included in the GFSM model. Intuitively, an increase in the overall complexity of the algorithms will be observed. Other kinds of equivalence may be investigated to reduce complexity in these cases 18 . Also, other techniques for complexity reduction may be investigated, such as statistical sampling based on randomization or hashing used in 16 This is one case where the correctness conditions for the model are sufficient but not necessary to meet the functional requirements for correctness, thus leading to a false error. Sufficiency and necessity proofs are subject of future work. 17 Repetition constructs include, for example, the '*' to represent zero or more states, or the '1+' to represent one or more states, '2+' two or more, so on. 18 An example of another kind of equivalence is fault dominance, where a system is proven to necessarily reach one error before reaching another, thus the former error dominates the latter error.
SPIN [14]. However, sampling techniques do not achieve full coverage of the state space.
• The topology used in this study is limited to a single-hop LAN. Although we found it quite useful to study multicast routing over LANs, the method needs to be extended to multi-hop LAN to be more general. Our work in [10] introduces the notion of virtual LAN, and future work addresses multi-LAN topologies.
In sum, the fault-independent test generation may be used for protocol verification given the symmetry inherent in the system studied (i.e., protocol and topology). For robustness studies, where the fault model is included in the search, the complexity of the search grows. In this approach we did not address performance issues or topology synthesis. These issues are addressed in the coming sections. However, we shall re-use the notion of forward search and the use of counting equivalence in the method discussed next.

V. Fault-oriented Test Generation
In this section, we investigate the fault-oriented test generation (FOTG), where the tests are generated for specific faults. In this method, the test generation algorithm starts from the fault(s) and searches for a possible error, establishing the necessary topology and events to produce the error.
Once the error is established, a backward search technique produces a test sequence leading to the erroneous state, if such a state is reachable. We use the FSM formalism presented in Section III to represent the protocol. We also re-use some ideas from the FITG algorithm previously presented, such as forward search and the notion of equivalence for search reduction.

A. FOTG Method Overview
Fault-oriented test generation (FOTG) targets specific faults or conditions, and so is better suited to study robustness in the presence of faults in general. FOTG has three main stages: a) topology synthesis, b) forward implication and error detection, and c) backward implication.
The topology synthesis establishes the necessary components (e.g., routers and hosts) of the system to trigger the given condition (e.g., trigger a protocol message The above pre-conditions can be derived automatically from the post-conditions. In Appendix III, we describe the 'PreConditions' procedure that takes as input one form of the conventional post-condition transition In cases where the stimulus affects more than one router (e.g., multicast P rune), multiple states need to be simultaneously implied in one backward step, otherwise an I.S.

B. FOTG details
As previously mentioned, our FOTG approach consists of three phases: I) synthesis of the global state to inspect, II) forward implication, and III) backward implication. These phases are explained in more detail in this section. In Section V-C we present an illustrative example for the these phases.

B.1 Synthesizing the Global State
Starting from a condition (e.g., protocol message or stimulus), and using the information in the protocol model (i.e. the transition table), a global state is synthesized for investigation. We refer to this state as the global-state inspected (GI ), and it is obtained as follows:

C. Applying The Method
In this section we discuss how the fault-oriented test gen-   Join topology synthesis, forward/backward implication Backward implication Losing the Join by the forwarding router R k leads to an error state where router Ri is expecting packets from the LAN, but the LAN has no forwarder.

C.3 Summary of Results
In this section we briefly discuss the results of applying Our method as presented here, however, may not be generalized to transform any type of timing problem into sequencing problem. This topic bears more research in the future.
We have used the sequences of events generated automatically by the algorithm to analyze protocol errors and suggest  Forward implication is then applied, and behavior after the crash is checked for correct packet delivery. To achieve this, host stimuli (i.e. SP kt, HJ and L) are applied, then the system state is checked for correctness.
In lots of the cases studied, the system recovered from the crash (i.e. the system state was eventually correct). The recovery is mainly due to the nature of PIM-DM; where protocol states are re-created with reception of data packets. This result is not likely to extend to protocols of other natures; e.g. PIM Sparse-Mode [15].
However, in violation with robustness requirements, there existed cases in which the system did not recover. In Figure 7, the host joining in (II, a) did not have the sufficient state to send a Graf t and hence gets join latency until the negative cache state times out upstream and packets are forwarded onto the LAN as in (II, b). Crash leading to join latency In Figure 8 (II, a), the downstream router incurs join latency due to the crash of the upstream router. The state is not corrected until the periodic broadcast takes place, and packets are forwarded onto the LAN as in (II, b).

Fig. 8
Crash leading to black holes

D. Challenges and Limitations
Although we have been able to apply FOTG to PIM-DM successfully, a discussion of the open issues and challenges is called for. In this section we address some of these issues. • The analysis for our case studies did not consider network delays. In order to study end-to-end protocols network delays must be considered in the model. In [10] we introduce the notion of virtual LAN to include end-to-end delay semantics.
• Minimal topologies that are necessary and sufficient to trigger the stimuli, may not be sufficient to capture all correctness violations. For example, in some cases it may require one member to trigger a Join, but two members to experience an error caused by Join loss. Hence, the topology synthesis stage must be complete in order to capture all possible errors. To achieve this we propose to use the symbolic representation. For example, to cover all topologies with one or more members we use (M 1+ ). Integration of this notation with the full method is part of future work. We believe that the strength of our fault-oriented method, as was demonstrated, lies in its ability to construct the necessary conditions for erroneous behavior by starting directly from the fault and avoiding the exhaustive walk of the state space. Also, converting timing problems into sequencing problems (as was shown for Graf t analysis) reduces the complexity required to study timers. FOTG as presented in this chapter seems best fit to study protocol robustness in the presence of faults. Faults presented in our studies include single selective loss of protocol messages and router crashes.

VI. Related Work
The related work falls mainly in the field of protocol verification, distributed algorithms and conformance testing. In addition, some concepts of our work were inspired by VLSI Protocol verification typically addresses well-defined properties, such as safety (e.g., freedom from deadlocks) and liveness (e.g., absence of non-progress cycles) [16]. In general, the two main approaches for protocol verification are theorem proving and reachability analysis (or model checking) [3] [4].
In theorem could be used. These techniques focus only on parts of the state space and may use probabilistic [24], random [25] or guided searches [26]. In our work we adopt approaches extending reachability analysis for multicast protocols. Our fault-independent test generation method (in Section IV) borrows from controlled partial search and state reduction techniques.
Work on distributed algorithms deals with synchronous networks, asynchronous shared memory and asynchronous networked systems [27]. Proofs can be established using an automata-theoretic framework. Several studies on distributed algorithms considered failure models including message loss or duplication, and processor failures, such as stop (or crash) failures, transient failures, or byzantine failures [28], where failed processors behave arbitrarily. We do not consider byzantine failures in our study. Distributed algorithms may be treated in a formal framework, using automata-theoretic models and state machines, where results are presented in terms of set-theoretic mathematics [27].
The formal framework is used to present proofs or impossibility results. Proof methods for distributed algorithms include invariant assertions and simulation relationships 26 that are generally proved using induction, and may be checkable using theorem-provers, e.g., Larch theorem-prover [29].
Several attempts to apply formal verification to network protocols have been made. Assertional proof techniques were used to prove distance vector routing [31], path vector routing [32] and route diffusion algorithms [33], [34] and [35] using communicating finite state machines. An example point-topoint mobile application was proved using assertional reasoning in [36] using UNITY [37]. Axiomatic reasoning was used in proving a simple transmission protocol in [38]. Algebraic systems based on the calculus of communicating systems (CCS) [39] have been used to prove CSMA/CD [40].
Formal verification has been applied to TCP and T/TCP in [41].
Multicast protocols may be modeled as asynchronous networks, with the components as timed-automata, including failure models. In fact, the global finite state machine (GFSM) model used by our search algorithms is adopted from asynchronous shared memory systems (in specific, cache coherence algorithms [13]) and extended with various multicast and timing semantics. The transitions of the I/O automaton may be given in the form of pre-conditions and effects 27 .
The combination of timed automata, invariants, simulation mappings, automaton composition, and temporal logic [42] seem to be very useful tools for proving (or disproving) and reasoning about safety or liveness properties of distributed algorithms. It may also be used to establish asymptotic bounds 26 An invariant assertion is a property that holds true for all reachable states of the system, while a simulation is a formal relation between an abstract solution of the problem and a detailed solution. 27 This is similar to our representation of the transition  Other related work includes verification of cache coherence protocols [13]. This study uses counting equivalence relations and symbolic representation of states to reduce space search complexity. We use the notion of counting equivalence in our study.

VII. Conclusions
In this study we have proposed the STRESS framework to integrate test generation into the protocol design process. More case studies are needed to show more general applicability of our methodology.

I. State Space Complexity
In this appendix we present analysis for the state space complexity of our target system. In specific we present completeness proof of the state space and the formulae to compute the size of the correct state space.

A. State Space Completeness
We define the space of all states as X * , denoting zero or more routers in any state. We also define the algebraic operators for the space, where A.1 Error states In general, an error may manifest itself as packet duplicates, packet loss, or wasted bandwidth. This is mapped onto the state of the global FSM as follows: 1. The existence of two or more forwarders on the LAN with one or more routers expecting packet from the LAN (e.g., in the N HX state) indicates duplicate delivery of packets.
2. The existence of one or more routers expecting packets from the LAN with no forwarders on the LAN indicates a deficiency in packet delivery (join latency or black holes).
3. The existence of one or more forwarders for the LAN with no routers expecting packets from the LAN indicates wasted bandwidth (leave latency or extra overhead).
-for duplicates: one or more N HX with two or more FX ; -for extra bandwidth: one or more FX with zero N HX; -for blackholes or packet loss: one or more N HX with zero FX ; A.2 Correct states As described earlier, the correct states can be described by the following rule: ∃ exactly one forwarder for the LAN iff ∃ one or more routers expecting packets from the LAN.
-zero N HX with zero FX ; -one or more N HX with exactly one FX ; from (B.2) and (B.3) we get: if we take the union of (B.8), (B.5) and (B.7), and apply (B.1) we get: also, from (B.4) and (B.2) we get: if we take the union of (B.10) and (B.6) we get: taking the union of (B.9) and (B.11) we get: which is the complete state space. To obtain the ErrorStates we can use: The percentage of the correct and error states

II. Forward Search Algorithms
This appendix includes detailed procedures that implement the forward search method as described in Section IV.
It also includes detailed statistics collected for the case study on PIM-DM.

A. Exhaustive Search
The ExpandSpace procedure given below implements an

Fig. 11
Simulation statistics for forward algorithms. The complexity of this procedure is given by (i.s.) n .

B. Reduction Using Equivalence
We use the counting equivalence notion to reduce the complexity of the search in 3 ways: 1. The first reduction we use is to investigate only the equivalent initial states, we call this algorithm Equiv. One procedure that produces such equivalent initial state space is the EquivInit procedure given below.    We call the algorithm after the third reduction the reduced algorithm.

C. Complexity analysis of forward search for PIM-DM
The number of reachable states visited, the number of transitions and the number of erroneous states found were recorded. The result is given in Figures 10, 11, 12, 13. The reduction is the ratio of the numbers obtained using the exhaustive algorithm to those obtained using the reduced algorithm.
The This means that we have obtained exponential reduction in complexity, as shown in Figure 14.

A. Pre-Conditions
The procedure described below takes as input the set of post-conditions for the FSM stimuli and genrates the set of pre-conditions. The 'conds' array contains the postconditions (i.e., the effects of the stimuli on the system) and is indexed by the stimulus.

C. Topology Synthesis
The following procedure synthesizes minimum topologies necessary to trigger the various stimuli of the protocol. It performs the third and forth steps of the topology synthesis procedure explained in Section V-B. were reachable. The statistics for the total and average number of backward calls, rewind calls and backtracks is given in Figure 15.
Although the topology synthesis study we have presented above is not complete, we have covered a large number of corner cases using only a manageable number of topologies and search steps.
To obtain a complete representation of the topologies, we suggest to use the symbolic representation 31 presented in Section III. Based on our initial estimates we expect the number of symbolic topology representations to be approximately 224 topologies, ranging from 2 to 8-router LAN topologies, for the single selective loss and single crash models.

F. Experimental statistics for PIM-DM
To investigate the utility of FOTG as a verification tool we ran this set of simulations. This is not, however, how FOTG is used to study protocol robustness (see previous section for case study analysis).
We also wanted to study the effect of unreachable states on the complexity of the verification. The simulations for our case study show that unreachable states do not contribute in a significant manner to the complexity of the backward search for larger topologies. Hence, in order to use FOTG as a verification tool, it is not sufficient to add the reachability detection capability to FOTG.
The backward search was applied to the equivalent error states (for LANs with 2 to 5 routers connected). The simulation setup involved a call to a procedure similar to 'EquivInit' in Appendix II-B, with the parameter S as the set of state 31 We have used the repetition constructs '0', '1', '*'.  Simulation statistics for backward algorithms symbols, and after an error check was done a call is made to the 'Backward' procedure instead of 'ExpandSpace'.
States were classified as reachable or unreachable. For the four topologies studied (LANs with 2 to 5 routers) statistics were measured (e.g., max, min, median, average, and total) for number of calls to the 'Backward' and 'Rewind' procedures, and the number of backTracks were measured. As shown in Figure 16, the statistics show that, as the topology grows, all the numbers for the reachable states get significantly larger than those for the unreachable states (as in Figure 17), despite the fact that that the percentage of unreachable states increases with the topology as in Figure 18.
The reason for such behavior is due to the fact that when the state is unreachable the algorithm reaches a dead-end relatively early (by exhausting one branch of the search tree).
However, for reachable states, the algorithm keeps on searching until it reaches an initial global state. Hence the reachable states search constitutes the major component that contributes to the complexity of the algorithm.

G. Results
We have implemented an early version of the algorithm in the NS/VINT environment (see http://catarina.usc.edu/vint) and used it to drive detailed simulations of PIM-DM therein, to verify our findings. In this section we discuss the results of applying our method to PIM-DM. The analysis is conducted for single selective message loss.
For the following analyzed messages, we present the steps for topology synthesis, forward and backward implication.

G.3 Graft
Following are the resulting steps for the Graf t loss: We did not reach an error state when the Graf t was lost, with non-interleaving external events.

H. Interleaving events and Sequencing
A Graf t message is acknowledged by the Graf t − Ack (GAck) message, and if not acknowledged it is retransmitted when the retransmission timer expires. In an attempt to create an erroneous scenario, the algorithm generates sequences to clear the retransmission timer, and insert an adverse event.
Since the Graf t reception causes an upstream router to become a forwarder for the LAN, the algorithm interleaves a Leave event as an adversary event to cause that upstream router to become a non-forwarder. Backward Implication: Using backward implication, we can construct a sequence of events leading to conditions sufficient to trigger the GAck. Hence, when a Graf t followed by a P rune is interleaved with the Graf t loss, the retransmission timer is reset with the receipt of the GAck for the first Graf t, and the systems ends up in an error state.