Formal Specification, Verification, and Automatic Test Generation of ATM Routing Protocol: PNNI

Authors Avatar

Formal Specification, Verification, and Automatic Test Generation of ATM Routing Protocol: PNNI

1. Introduction

For the reliability of ATM networks, there is an urgent need to apply some formal methods in validating these protocols and in generating test cases. The tools needed to accomplish these purposes include: a technique to model the protocol, a formal description language to describe the model, a protocol simulator to perform verifications, and a test generator to produce test cases. This work is a case study of applying formal verification and test generation tools to the ATM network routing protocol, or the ATM Forum Private Network-Network Interface (PNNI) Specification Version 1.0 [1].

The PNNI specification consists of three layers of protocols: the Hello protocol for identifying the status of NNIs; the Database Synchronization protocol for maintenance of routing databases; and the Peer Group Leader Election protocol for operations of hierarchical routing. Each of the PNNI sub-protocols can best be modeled as communicating Extended Finite State Machines (EFSM) with parameters [2]. The system behavior of the PNNI protocol system is the combined effects of three communicating EFSMs. The issue at hand is: Is it necessary to develop a complete composite state machine to correctly model PNNI, and if so, how? Furthermore, since a PNNI system represents an ATM network switching node, within a network switching nodes are expected to interact with each other. Therefore what is the minimum number of nodes needed to correctly simulate the operation of PNNI?

In our study, we take two nodes connected by a full-duplex channel, based on the following observations. We want to detect design/specification errors from verification, implementation errors from conformance testing, and errors from both the design and implementation from interoperability testing. Suppose that an error is revealed using a two-node model, then obviously, faults in the specification are detected. Conversely, suppose that there are faults in PNNI in a multiple node network. Since it is a hierarchical protocol, we can group the nodes into two peer groups. Each peer group then behaves like a single node. These two connected peer groups behave like our previous two nodes, so the faults will manifest in this two-node network as well. Therefore, we confine ourselves to a two-node network for our verification and testing study.

The tool set we use is PROMELA, SPIN [3] [5], and PITHIA [4] for modeling, simulating, and generating tests for the protocols, respectively. The rest of this paper is organized as follows: section 2 presents a brief introduction of the PNNI protocols; section 3 presents the development of the models, processes and results of simulations using SPIN; section 4 describes the process of test generation from the reachability graph; and section 5 presents concluding remarks.

2. Private Network-Network Interface 1.0

The Private Network-Network Interface (PNNI) is a set of protocols that define the dynamic distribution of routing information and the signaling used, once the routing information is complete. These routing protocols are a derivation of protocols used in the Internet. The signaling protocols are not studied in this project.

The routing protocols dynamically obtain, distribute, and summarize information about the nodes (i.e. ATM switches) and the links connecting these nodes. A hierarchy mechanism is used to reduce the amount of information that has to be distributed. This hierarchy mechanism is built upon groupings of switches into peer groups. Within a peer group all switches share the same routing information. A peer group can be viewed by other switches as a single logical switch. This single logical switch can itself be a member of another higher level peer group. This process continues, thus building a hierarchy.

There are three main protocols for accomplishing the task of routing. They are the Hello Protocol, the Database Synchronization Protocol including Flooding, and the Peer Group Leader Election (PGLE) Protocol. These protocols all interact.

2.1 Hello Protocol

The Hello protocol’s purpose is to discover and to verify the identity of the neighboring node at the other end of a physical link or virtual path connection, as well as to maintain the status of its connectivity to that neighboring node. The information learned about the other node includes its ATM address, node identity, port identity, peer  group identity. Other information is also passed but is not used immediately by the Hello protocol.

The Hello protocol can be divided into two parts: an inside part where the two neighboring nodes are within the same peer group, and an outside part where the two neighboring nodes are in different peer groups. For the latter there are two further possibilities. The two neighboring nodes may either share a common higher level peer group or not. Two neighboring nodes that are in different peer groups are called border nodes.

The Hello protocol is the first protocol to run once a link between two neighboring nodes is active. The Hello protocol operates on a per link basis.

2.2 Database Synchronization and Flooding

The Database Synchronization protocol’s purpose is to distribute the currently  known routing information between two neighboring nodes that are in the same peer group. When the database synchronization process is complete both neighboring nodes will have exactly the same routing information. The Flooding procedures are the necessary extensions to the database synchronization protocol in order to keep all routing information within a single peer group current.

The Database Synchronization protocol is started with the event AddPort, which is generated when the first link between two neighboring nodes running the Hello protocol enters the state, Two Way Inside. The synchronization of the databases is done through the exchange of Database Summary (DS) packets. These describe the PNNI Topology State Elements (PTSEs) that a node has in its database. In response to these packets a node requests the PTSEs that it does not have from its neighbors. The other nodes respond to these requests by sending the appropriate PTSEs in PNNI Topology State Packets (PTSPs). After these exchanges the databases will be synchronized.

This protocol runs between a pair of neighboring nodes, not on a per link basis and thus can involve more than one link. The two neighboring nodes form a Master/Slave relationship for the distribution of the routing information.

2.3 Peer Group Leader Election

Join now!

The Peer Group Leader Election protocol provides a mechanism for choosing one node from within a single peer group to represent the other nodes as a single logical  group node. This elected node, or Peer Group Leader (PGL) will then perform other functions for building a hierarchical network topology.

Normally all the nodes of the peer group participate in the peer group leader  election. Each node is configured with a peer group leadership priority value, which indicates its desirability to become PGL. There are two configurations for a node. Either the node does not want to be PGL and ...

This is a preview of the whole essay