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

Published

November 1, 1998

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

Pub Type

Conferences

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 December 3, 2024)