Protocols for Highly available distributed call processing systems

Abstract

In telecom applications, a key requirement of any call processing system is high availability; an order of “five nines” availability is needed. With the evolution of Next Generation Networks (NGN), the current trend in the telecom industry is the decomposition of the call processing and bearer functionalities. The availability of cheaper and more reliable commercial off-the-shelf components (COTS) has led to their use in building highly available call processing systems, such as soft switches. For call processing packet-based nodes, the industry is still using proprietary architectures and there are no standard common techniques to provide high availability. This results in higher complexity and effort in understanding, developing, and maintaining such systems. In our work, we aim to obtain a solution to the generic problem of providing high availability feature for packet-based call processing systems. The requirements of these systems are analyzed, and it is established that HA-OSCAR cluster architecture is suitable for building the packet-based call processing nodes. The HA-OSCAR architecture consists of two server nodes (SNs) and a few application nodes (ANs) that are connected via a duplicated interconnection medium, possibly a Local Area Network (LAN). Based on the architecture, the detailed requirements of call processing systems are then obtained. We specify the following protocols between the various entities of the system model, which enables the system to meet its requirements:

Server-Server System Management protocol Server-AN System Management protocol Session Handling protocol Server-Server Session Handling protocol Server-AN Session Handling protocol AN-AN Session Handling protocol

The above-mentioned protocols are specified with the help of state machines, procedures, messages and timers. Since the protocols were very complex, it was necessary to use formal verification techniques to ensure that they work correctly and have desired properties. For such purposes, the Simple Promela Interpreter (SPIN) model checker is an appropriate verification tool. In our work, we modeled the protocols using the modeling language Process or Protocol Modeling Language (Promela), identified the requirements for correctness of the protocols, and then formulated the properties using Linear Temporal Logic (LTL). Formalizing the model and the properties, performing the verification process, and analyzing it for our complex system was an iterative process and required a lot of effort. The verification model did not run with SPIN in its original form; modification was required in the SPIN tool itself, to include the concept of discrete time, and even the model had to be modified to suit the needs of the tool. The size and complexity of the system of protocols precluded its exhaustive verification as a single entity. The composite model was replaced by a set of reduced models, each of which was used to verify a subset of protocols. Optimization techniques provided by SPIN were used to attempt exhaustive verification of the protocols. Even with all such efforts, while exhaustive verification of Server-Server System Management protocol could be achieved, it was not possible for the Server- AN System Management protocol and Session Handling protocol, which were partially verified using bitstate hashing technique. The bugs found during the verification process were corrected and the corrected model is proposed with more confidence. In this work, we have provided a structured roadmap for proposing, specifying, and verifying the system model and protocols to meet the requirements of call processing systems. We have verified that the proposed protocols satisfy the desired properties, thereby establishing the relevance of formal verification in the area of protocol design and call processing telecom systems.