No abstract available.

Passive testing is a process of detecting faults in a system under test by passively observing its input/output behaviors only without interrupting its normal operations, and proves to be a promising technique for network fault management. We study passive testing of data portions of network protocols and present two algorithms, using an event-driven extended finite state machine model. Experimental results on the Internet routing protocol OSPF (open shortest path first) are reported.

We propose and analyze formal models for coordination functions of the 802.11 MAC layer using systems of communicating machines. We model the basic DCF (CSMA/CA) protocol, the DCF (distributed coordination function) protocol with RTS/CTS (MACA), and the PCF (point coordination function) protocol. Analyses show the following safety results: the CSMA/CA protocol is free from deadlocks and non-executable transitions; the MACA has a potential livelock, but is free from deadlocks and non-executable transitions; the PCF protocol is free from deadlocks and non-executable transitions. We also show that liveness is guaranteed in the PCF protocol.

In this paper, we employ the communicating finite state machine (CFSM) model for networks to investigate fault management using passive testing. First, we introduce the concept of passive testing. Then, we introduce the CFSM model, the observer model and the fault model with necessary assumptions. We introduce the fault detection algorithm using passive testing. Then, we briefly present our new passive testing approach for fault location, fault identification, and fault coverage based on the CFSM model. We illustrate the effectiveness of our new technique through simulation of a practical protocol example, a 4-node mobile IPv6 network. Finally, conclusions and potential extensions are discussed.

This paper introduces an approach for protocol performance estimation directly from a formal model of the protocol. By using the approach presented in this paper, performance of a protocol can be quickly estimated at an early stage of protocol design. The simplicity of analysis, achieved by deterministic analysis, and the tight integration of the performance model, called the performance reachability graph (PRG), with the formal specification makes the approach in this paper a very useful protocol design-time tool. The approach provides a two way path between the specification model and the performance model. In one direction, the tight coupling between the specification and the performance models allows a protocol designer to get quick estimates of performance from the specification. In the other direction a designer can use the performance estimates to quickly identify portions of the specification responsible for undesired performance characteristics and consider changes to the specification to improve the overall performance.

In protocol composition techniques, component protocols are combined in various ways to obtain a complex protocol whose execution sequences consist of interleaved execution sequences of the component protocols. We investigate the problem of verifying liveness properties of the composite protocol from the known properties of its components. We first characterize a class of composition techniques that encompasses almost all composition techniques that have appeared in the literature. We then develop a sufficient condition to ensure that certain liveness properties of the component protocols carry over to the composite protocol. A proof technique, based on this sufficient condition, is then used to determine whether the liveness properties of the component protocols also hold for the composite protocol. To demonstrate the usefulness of our technique, we use several protocols including synchronizing, ordering and disabling protocols as examples. The technique is applicable to any transition based protocol model as long as the model is susceptible to reachability analysis for the sake of correctness proofs.

We propose a specification model and present a method to algorithmically derive a protocol specification from a service specification based on the model. Unlike the previous models based on finite state machines, the proposed model can explicitly express concurrency, synchronization, and timing requirements such as delays and timeouts. We assume that there exists a reliable communication channel between say two protocol entities and the maximum delay for each channel is bounded by a positive constant. Because of the variable nature of the communication delays along with the time constraints associated with events, no protocol specification can fully simulate the service specification. The proposed method derives a protocol specification that is optimal in the sense that it provides the largest possible subset of the service specification under the communication delay constraints. We also give a method to derive a sub specification from a service specification and a maximum communication delay of each channel such that the sub specification, but no superset of it, can be simulated by the derived protocol specification.

We propose a framework based on the model of timed extended finite state machines for building communication protocols which perform several functions, where each function corresponds to a component protocol. For parallel composition, we specify a conjunctive relation which requires that the execution of events in two component protocols be synchronized. We also propose a predicate strengthening technique to refine the composite protocol in a stepwise manner while preserving the invariants of the component protocols. For sequential composition, we present a set of constraints, alternating, ordering and disabling, on the actions of the component protocols, and give sufficient conditions for the composite protocol to retain the safety properties such as freedom from unspecified receptions and freedom from deadlocks. Our sufficient conditions are weaker than those given an previous works.

We generalize the technique of fair reachability analysis to multi-cyclic protocols modeled as networks of communicating finite state machines, where a number of cyclic protocols are interconnected in such a way that any two component cyclic protocols share at most one process and each channel in the protocol belongs to exactly one component cyclic protocol. By composing the fair reachability relations of the component cyclic protocols, we prove that the set of fair reachable states of a multi-cyclic protocol is exactly the set of reachable states that are of equal channel length with respect to each of its component cyclic protocols. As a result, each deadlock state is fair reachable, and deadlock detection is decidable for the class of multi-cyclic protocols whose fair reachable state spaces are finite. Under the assumption that the underlying communication topology of a protocol is strongly connected, we show that fair reachability analysis is inherently infeasible for logical correctness validation beyond multi-cyclic protocols.

We adapt the partial order state reduction techniques developed for Petri nets and labeled transition systems to the validation of multi-process protocols modeled as communicating finite state machines. We identify two specific partial order reduction methods in this context: (1) maximal partial order reachability analysis, which is a generalization of maximal reachability analysis to protocols with n/spl ges/2 processes; and (2) simultaneous partial order reachability analysis, which is a counterpart of fair reachability analysis for protocols with n/spl ges/2 processes and arbitrary communication topologies. We study the logical error detection capabilities of each method and show that these two methods, when used together, provide complete logical error coverage for bounded multi-process protocols.

In this paper, the notion of fair reachability is generalized to cyclic protocols with n/spl ges/2 machines. It is shown that each fair reachable state is of equal channel length and each deadlock state is fair reachable. As a result, deadlock detection is decidable for P, the class of cyclic protocols whose fair reachable state spaces are finite. The concept of simultaneous unboundedness is defined and the lack of it is shown to be a necessary and sufficient condition for a protocol to be in P. Through finite extension of the fair reachable state space, it is also shown that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for P. Furthermore, it is shown that any protocol in P is logically correct if and only if there is no logical error in its fair reachable state space. This study demonstrates that for the class P, our generalized fair reachability analysis technique not only can achieve substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a very useful technique to prove logical correctness for a wide variety of cyclic protocols.

We study three reachability problems for cyclic protocols: (1) global state reachability; (2) abstract state reachability; and (3) execution cycle reachability. By combining fair progress and maximal progress during state exploration, we prove that these three problems an all decidable for Q, the class of cyclic protocols with finite fair reachable state spaces. In the course of the investigation, we also show that detection of k-indefiniteness and k-livelock an decidable for Q.

In this paper, we extend the generalized fair reachability notion to cyclic protocols with nondeterministic and internal transitions. By properly incorporating internal transitions into the formulation of fair progress vectors, we prove that with only a few modifications, all the results established for cyclic protocols without nondeterministic and internal transitions still hold even if nondeterministic and internal transitions are allowed. We identify indefiniteness as a new type of logical error resulting from reachable internal execution cycles and show that it can also be detected for the class of cyclic protocols with finite fair reachable state spaces with finite extension.

In a previous paper, we generalized the fair reachability notion to cyclic protocols with n/spl ges/2 machines and showed that deadlock detection is decidable for /spl Pscr/, the class of cyclic protocols whose fair reachable state spaces are finite. In this paper, we show that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for class /spl Pscr/ via finite extension of the fair reachable state space. This study shows that for the class /spl Pscr/, our generalized fair reachability analysis technique not only achieves substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a viable state reduction technique.>

A theoretical analysis of the fault coverage of conformance test sequences for communication protocols specified as finite state machines is presented. Faults of different types are considered, and their effect on testing is analyzed. The interaction between faults of different categories and the impact it has on conformance testing is investigated. Fault coverage is defined for the testing of both incompletely-specified machines (ISMs) and completely-specified machines (CSMs). An algorithm is presented to generate test sequences with maximal fault coverage for the testing of ISMs. It is then augmented for the testing of CSMs, and finally a technique is presented for generating test sequences which provides guaranteed maximal fault coverage for the conformance testing of communication protocols.>

This paper focuses on a technique to reduce the length of maximal fault coverage test sequences for communication protocols by removing redundant test segments. This approach conceptually begins with all the test segments needed for the generation of maximal fault coverage test sequences, analyzes the structure of the specified finite state machine for the protocol, and shows that certain segments in these tests are unnecessary to guarantee maximal fault coverage. From this analysis an algorithm is proposed for generating the reduced length sequences that still guarantee maximal fault coverage. The authors describe how these tests are in some sense minimal, or near minimal, length test sequences without losing fault coverage.>

A model for the specification and analysis of communication protocols called Systems of Communicating Machines is used to specify a CSMA/CD (carrier-sense multiple access with collision detection) protocol, and to analyze it for safety and certain restricted liveness properties. The model uses a combination of finite state machines and variables in the specification of each machine, and the communication between machines is accomplished through shared variables. The Ethernet bus is modeled as a single variable shared by all communicating processes. Collisions are modeled by simultaneous writes to this variable.>

A technique for generating a test sequence for conformance testing of communication protocols is presented. This approach shows that it is possible to generate optimal-length test sequences which include multiple unique input/output (UIO) sequences and overlapping under certain conditions. In the absence of the above-mentioned conditions, a heuristic technique is used to obtain suboptimal solutions which show significant improvement over optimal solutions without overlapping. The technique is illustrated by the example of the NBS Class 4 Transport Protocol (TP4). The computational complexity of the algorithm is compared with that of previous techniques. A brief discussion of bounds on test sequence length is presented, and the results are compared with these bounds.>

A new technique of generating a test sequence for conformance testing of communication protocols is presented. This approach shows that it is possible to generate optimal length test sequences which include multiple unique input output sequences that overlap under certain conditions. In the absence of these conditions, a heuristic technique is used to obtain sub-optimal solutions, which show significant improvement over optimal solutions without overlapping. A comparison is also made of the computational complexity of the author's algorithm with that of existing techniques. A brief discussion of bounds on test sequence length is presented and results are compared against these bounds.>

Communicating finite state machines (CFSM's) with FIFO (first in, first out) queues are used to model a protocol converter. A protocol conversion algorithm is developed and presented for the CSFM model of the protocols A and B. A converter H for protocols A=(A/sub 0/, A/sub 1/) and B=(B/sub 0/, B/sub 1/) is viewed as a black box such that H is between sender A/sub 0/ and receiver B/sub 1/. This gives a resulting protocol X=(A/sub 0/, H, B/sub 1/). The conversion algorithm requires a specification of the message relationships between the messages of protocols A and B. It is assumed that protocols A and B have the required progress properties. The algorithm includes a search for related messages from the two protocols in an FIFO from a composite space formed by a Cartesian cross-product of state spaces A/sub 1/ and B/sub 0/. The search produces finite-length traces which are combined to form a state machine H, which is examined for freedom from unspecified receptions, deadlocks, and livelocks. A protocol conversion example demonstrates the applicability of the algorithm.>

A window protocol based on the block acknowledgment method, in which acknowledgment message has two numbers, m and n, to acknowledge the reception of all data messages with sequence numbers ranging from m to n, is discussed. In the window protocol, message sequence numbers are taken from a finite domain and both message disorder and loss can be tolerated. An initial version of the protocol that uses a simplified timeout action and unbounded sequence numbers is presented, the simplified timeout action in the protocol is replaced by a sophisticated one without disturbing the protocol's correctness, and the unbounded sequence numbers are replaced by bounded ones while preserving the protocol's correctness. Remarks concerning other variations of the protocol are also presented.>

We describe a new version of the window protocol where message sequence numbers are taken from a finite domain and where both message disorder and loss can be tolerated. Most existing window protocols achieve only one of these two goals. Our protocol is based on a new method of acknowledgement, called block acknowledgement, where each acknowledgement message has two numbers m and n to acknowledge the reception of all data messages with sequence numbers ranging from m to n. Using this method of acknowledgement, the proposed protocol achieves the two goals while maintaining the same data transmission capability of the traditional window protocol.

No abstract available.

Finite state automata have been applied with success to the modeling of Computer Network Protocols. The interaction of finite state machines can be very complex especially if the protocol involves a large number of states. To counteract the complexity of analysis and design, we propose an approach of decomposition. Through this approach, the protocol graph can be partitioned into subgraphs each having a unique entry node and zero or more exit nodes. The exit nodes of one subgraph can be connected only to the entry nodes of other subgraphs. From the standpoint of protocol analysis, the correctness of the entire protocol graph can be inferred from the correctness of individual protocol subgraphs. From the standpoint of protocol design, the individual protocol subgraphs can be designed to correspond to different phases of the protocol. If the individual protocol subgraphs are designed correctly and the connections between subgraphs conform to the structure discussed above, then we show that the entire protocol graph will operate correctly.

Since the early 1960's many different models of parallel computation have been developed, some being based on finite state n1achine approaches, others on program schemata models, with many having underlying directed graph representations.[1,2,7,8,10,14,16,17] On the surface these models often appear quite different from one another. Also, the particular types of parallelism problems studied, and the results obtained, seemed often to bear no relation to one another. Thus, the area of modelling parallel computation seemed rather fragmented. In attempts to help unify the area, papers have been written comparing the various models and showing relationships between them. [2.9-13,15] Thus, results obtained in terms of one model often could be translated into results in another model. It is fairly well known by now, for example, that vector addition systems are in some sense "equivalent" to Petri nets,[6,13,16] and that some of the other graphical models for parallel computation are somehow "less powerful" than Petri nets or vector addition systems. This paper presents a comparative study of models of parallel computation using a rather general notion of a homomorphism between computation systems. This notion provides a precise relationship of one computation system being simulated by another computation system. In comparison to previous studies, this approach provides a more precise and deeper understanding of how the properties of the various models are interrelated. Many of the previously discovered relationships follow as corollaries of results obtained here. In particular, the concept of an "isomorphism" between two models turns out to be a particular type of homomorphism which is shown to be both length preserving and bijective. Results in this paper that may be of particular interest include a long list of properties that are preserved under homomorphism, that vector replacement systems can be simulated by vector addition systems, and that generalized Petri nets can be simulated by Petri nets. Here we outline our approach without giving all the precise definitions, and we omit all proofs. A more complete account is given in [9].

The 2,3-trees that are optimal in the sense of having minimal expected number of nodes visited per access are characterized in terms of their “profiles”. The characterization leads directly to a linear-time algorithm for constructing a K-key optimal 2,3-tree for a sorted list of K keys. A number of results are derived that demonstrate how different in structure these optimal 2,3-trees are from their “average” cousins.

When studying parallel computation and synchronization one is faced with the problem of modeling the simultaneous execution of processes. Although there has been a multitude of formal means for representing such problems [2, 6, 9, 10, 13, 14, 15], invariably, when all the other complexities of the models have been stripped away, the parallelism or synchronization is studied via sequences of events.

A model is defined in which questions concerning delay bounded asynchronous parallel systems may be investigated. Persistence and determinacy are introduced for this model. These two conditions are shown to be sufficient to guarantee that a synchronous execution policy can be relaxed to an asynchronous execution policy with no change to the result of the computation. In addition, the asynchronous execution time is only (D+1) times the synchronous execution time, where D is the delay bound. A wide class of recognition problems is identified which can be solved by linear asynchronous structures. Also, it is shown that synchronization problems, similar to the "firing squad synchronization problem," cannot be solved by delay bounded asynchronous systems.

In this paper we briefly describe and compare a number of theoretical models for parallel computation; namely, Petri nets, computation graphs, and parallel program schemata. We discuss various problems and properties of parallel computation that can be studied within these formulations and indicate the ties between these properties and the more practical aspects of parallel computation. We show how marked graphs, a particular type of Petri net, are a restricted type of computation graph and indicate how some results of marked graphs can be obtained from known results of computation graphs. Also, for schemata we discuss the decidability versus undecidability of various properties and several techniques of schemata composition.

In this paper we look at a number of matching problems and devise general techniques for attacking such problems. In particular, we describe a strategy for constructing efficient algorithms for solving two types of matching problems. We use this strategy to develop explicit algorithms for these two problems applied to strings (where the patterns are substrings) and arrays (where the patterns are subarrays or blocks). We also develop algorithms for these and related problems for trees, where the patterns are subtrees. Certain special cases of these algorithms are also discussed.

Some theorems showing undecidability for computational commutativity, boundedness, termination and determinacy of parallel program schemata are proved. These results are then compared with contrasting decidability results in [1] showing that the deletion of the hypothesis of repetition-freeness from the decidability theorems produces undecidability.

A set equations in the quantities a i ( p ), where i = 1, 2, · · ·, m and p ranges over a set R of lattice points in n -space, is called a system of uniform recurrence equations if the following property holds: If p and q are in R and w is an integer n -vector, then a i ( p ) depends directly on a j ( p - w ) if and only if a i ( q ) depends directly on a j ( q - w ). Finite-difference approximations to systems of partial differential equations typically lead to such recurrence equations. The structure of such a system is specified by a dependence graph G having m vertices, in which the directed edges are labeled with integer n -vectors. For certain choices of the set R , necessary and sufficient conditions on G are given for the existence of a schedule to compute all the quantities a i ( p ) explicitly from their defining equations. Properties of such schedules, such as the degree to which computation can proceed “in parallel,” are characterized. These characterizations depend on a certain iterative decomposition of a dependence graph into subgraphs. Analogous results concerning implicit schedules are also given.

A procedure for index register allocation is described. The rules of this procedure are shown to yield an optimal allocation for “straight line” programs.

In recent years adaptive threshold ele-ments have been used as the basis for learning machines such as the Perceptron [1] and Adaline [2]. To the author's knowledge there has been no previously reported work on a systematic study of algorithms, used in learning machines, to modify the weightvalues of threshold elements.

Formal procedures for the analysis and synthesis of two-terminal combinational bilateral switching networks are presented. A bilateral switching network is one which contains only elements having the same switching transmission characteristic in both directions. Following the definitions for the terminology and notation, where some new terms are introduced, the definitions for a series-parallel network, a bridge element, and a bridge network are given. A condition, called the bridge condition, to test a given transmission function for possible bridge network realizations is presented. A stepwise decomposition procedure is developed which may be used for the analysis and synthesis of the series and parallel parts of the network. The steps are described both with linear graphs and connection matrices. The bridge condition partially formalizes bridge network synthesis. Redundant variables also are considered as an aid to network synthesis. Under certain conditions, the synthesis yields network realizations with the fewest possible number of elements.