Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

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

Published

Author(s)

David E. Cypher, Dongjin Lee, M Martin-Villalba, C A. Prins, David H. Su

Abstract

This paper presents an effort to use formal tools to model, validate,and generate test suites for the ATM network routing protocol calledPrivate Network-Network Interface (PNNI). PNNIconsists of three layers of protocols: the Hello protocolfor identifying the status of NNIs; the Database Synchronization protocolfor maintenance of routing databases; and the PeerGroup Leader Election protocol for operations of hierarchical routing. Parameterized extended finite state machine (EFSM) models were developed for each protocol using the PROMELA language; communicating EFSM's are used to model all PNNI protocols. The models were executed using the SPINsimulator, which performs protocol validations and generates reachability graphs. It simulates two network nodes communicating with each other. The reachability graph for the Hello protocol model was produced and fed into anautomatic test case generation tool, PITHIA, to produce test cases. This paper discusses some of the problems encountered while implementing the models and their solutions, such as state space explosion and lack of modeling powerof timers in PROMELA.
Proceedings Title
Proceesings FORTE/PSTV '98 Tutorials & Eductional Case Studies in Protocols
Conference Dates
November 3-6, 1998
Conference Location
Paris, FR
Conference Title
FORTE/PSTV Tutorials & Eductional Case Studies in Protocols

Keywords

conformance and inoperability test, modeling, protocol verification, test suite generation

Citation

Cypher, D. , Lee, D. , Martin-Villalba, M. , Prins, C. and Su, D. (1998), Formal Specification, Verification, and Automatic Test Generation of ATM Routing Protocol: PNNI, Proceesings FORTE/PSTV '98 Tutorials & Eductional Case Studies in Protocols, Paris, FR (Accessed April 14, 2024)
Created November 1, 1998, Updated February 19, 2017