Specification and validation of Q.2931 ATM signaling protocol using estelle

ATM, which stands for Asynchronous Transfer Mode, is a networking technology widely considered to be the most promising and efficient method of transporting information through future telecommunication networks. An important part of its definition is a signaling mechanism, which is used to set up and release ATM connections. ITU-T defined a signaling protocol Q.2931, which is designated as an official standard for call control in both public and private versions of the ATM User Network Interface (UNI).The main goal of this thesis is to specify formally the signaling protocol in Estelle--one of the Formal Description Techniques (FDT). A specification written in an FDT offers great advantages as compared to an informal one. It is unambiguous; it may be used for protocol simulation and validation; and it may also serve as a basis for an actual implementation.In this study, we design and create a formal specification of the Q.2931 ATM signaling protocol. To demonstrate its signaling functionalities, we develop a simulation model representing the working environment of the protocol. We propose a validation methodology, which we use to show the conformance of our description to the requirements of the official protocol definition. Finally, we present observations and conclusions gathered as results of our experiments