Authors:
D. Cypher, D. Lee, M. Martin-Villalba, C. Prins, and D. Su

This paper presents an effort to use formal tools to model, validate, and generate test suites for the ATM network routing protocol called Private Network-Network Interface (PNNI). PNNI consists of three layers of protocols: the Hello protocol for identifying the status of NNIs; the Database Synchronization protocol for maintenance of routing databases; and the Peer Group 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 SPIN simulator, 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 an automatic 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 power of timers in PROMELA.