| dc.description.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. | |
