Specification and Verification of Generic Cell Rate Algorithms in PVS

Formal verification methods have been considered as a powerful complementary approach to define standards and to prove correctness of the systems. In this work, formal specification of Generic Cell Rate Algorithms are defined and proved. The specification process enables standardization for constructing Generic Cell Rate Algorithms. Standardization is an important process in the Asynchronous Transfer Mode (ATM) networks. By employing formal methods, the necessary standards could be constructed to allow different algorithms to be employed which still meet system requirements. Those system requirements are quantified in the Quality of Service (QOS). Congestion management is a vital concept for networks in that when the congestion occurs it would collapse the network performance. ATM network resources that can become congested include switch ports, buffers, transmission links, ATM layer processors and connection admission control processors. In ATM, congestion is defined as the condition where the offered load approaches or exceeds the network design limits for guaranteeing the Quality of Service (QOS) specified in the traffic contract. In order to avoid congestion at the cell base, the users' contracted network parameters must be monitored to ensure that the users obey their contracts. Otherwise, the network should take an action to the cells by tagging or discarding. These actions are termed User Parameter Control (UPC) functions. The most common Usage Parameter Control function is the Generic Cell Rate Algorithm (GCRA). It has advantage over other UPC functions because of its simplicity of hardware along with its quick response time. This thesis concentrates on Generic Cell Rate Algorithms, applying formal verification methods. Formal methods are used to build a specification model of GCRA and prove desired properties of the system. The Prototype Verification System (PVS) is chosen providing a specification language, a type checker, and a mechanical theorem prover. Some of the benefits of PVS include: the ability to represent abstract modeling connections, the advantage of building modular representations and using the libraries, and the ability to create requirements on future designs. In the present study the GCRA algorithms Virtual Scheduling and Leaky bucket are separate]y specified and certain properties are verified. It is shown that analyzing with PVS can provide complete coverage and understanding of the Generic Cell Rate Algorithm. In addition to this confidence of knowledge about GCRA, this work provides necessary background to improve the functionality of GCRA.