Applying formal methods to a protocol standard and its implementations

We explore the use of formal methods in the analysis of the SONET Automatic Protection Switching (APS) protocol. Unlike most protocol studies, we look at both conformance and interoperability aspect of APS. We use the Concurrency Workbench of North Carolina (R. Cleveland and S. Sims, 1996) to show proper interoperation of network elements running the protocol, and use the VeriSoft tool (P. Godefroid, 1997) to show conformance of Lucent Technologies APS implementation to the APS standard. We define a new notion of conformance, identify problems with APS, suggest general improvements to the structure of protocol standards, and suggest how protocol implementations can be written to allow conformance checks to be automated