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

1. Introduction
For the reliability of ATM networks, there is an urgent need to apply some formal methods in validating these protocols and in generating test cases. The tools needed to accomplish these purposes include: a technique to model the protocol, a formal description language to describe the model, a protocol simulator to perform verifications, and a test generator to produce test cases. This work is a case study of applying formal verification and test generation tools to the ATM network routing protocol, or the ATM Forum Private Network-Network Interface (PNNI) Specification Ve…