Automated generation of protocol test sequences from formal specifications

A program which takes as input the formal specification of a protocol using the formal model systems of communicating machines, and outputs a sequence of tests for an implementation of the protocol is discussed. The protocol is specified formally as a finite state machine with local and shared variables. The test program, called TESTGEN, finds all paths which may be taken through the FSM and generates a sequence of tests to check all these paths. Certain possible error conditions or difficult to test conditions are also detected by the program, and the test designer receives a warning message. The program is applied to a formal specification of the CSMA/CD and FDDI protocols, generating a test sequence for both of these protocols