FINITE STATE MACHINE BASED FORMAL METHODS IN PROTOCOL CONFORMANCE TESTING - FROM THEORY TO IMPLEMENTATION

Recent evolution of communication networks has led toward increasingly complex communication protocols to interconnect heterogenous systems. In order for such systems to function properly, communication protocols require formal methodologies for verification, implementation and testing. In this paper, the use of formal methods for protocol conformance testing is presented. Four major formal techniques for conformance test generation reported in the literature are compared: transition tours, distinguishing sequences, characterizing sequences and unique input/output sequences. The implementation of each approach as a test generation methodology is illustrated. The result is the capability to generate abstract test suites that require a minimum number of steps to execute while maintaining complete coverage of the state transitions (or test purposes) of the protocol. The impact of the formal methodologies on the practical aspects of conformance testing, including the test system implementation and automatic test script generation, is discussed. The experience based on testing various protocol implementations from multiple manufactures at AT&T Bell Laboratories is described. The protocols tested include X.25 and ISDN Q.921 and Q.931 for basic and primary rate interfaces. In order to standardize various efforts on conformance testing, the ISO and the CCITT have developed principles to specify abstract and executable test suites, and methodologies to design testbed architectures. The relationship between such standards and the formal methods for test generation is explored.