This thesis is concerned with verifying the correctness of human designed test cases for determining the conformance of a protocol implementation with its formal specification. Correctness of a test case, like any other software systems, is established by verifying the safety and liveness properties of the test case against the model of a test verification system.

A test verification system is derived from the architectural basis of the test case by representing the Lower Tester as an extended finite state machine (EFSM), substituting the implementation under test by the EFSM model of the corresponding protocol specification, representing the Upper Tester as an EFSM model derived either from the test case or from the test management protocol depending on the test architecture, modeling the input/output service specification of the underlying service provider as an EFSM, and representing each interaction point between two EFSMs in the test architecture by two FIFO channels. Algorithms are presented to derive EFSMs from the Estelle specifications of protocols and Tree and Tabular Combined Notation (TTCN) descriptions of test cases.

The model of a test verification system represents the global state space of the verification system with a set of atomic predicates associated with each global state, such that a global state's atomic predicates evaluate to true in that state. An algorithm, based on the well known reachability analysis technique, is presented to derive the global state space of a test verification system.

Four types of test case safety properties are defined:​ transmission safety, reception safety, synchronization safety, and verdict safety. The first two types of safety properties are common to all communication systems and the latter two are specific to protocol test systems. The liveness property of a test case is based on the idea that the test case behavior leading to a Pass test verdict fulfills the test purpose. We have proposed a set of notations to represent the safety and liveness properties as formulas in branching time temporal logic.

Test case properties are verified on the model of a test verification system by using a model checking algorithm. A methodology is also discussed to verify multiplexing test cases used in a multi-party test environment.

The verification methodology is applied to three test cases:​ one Remote Single-layer (RS) architecture based test case for an Association Control Service Element (ACSE) protocol, one Coordinated Single-layer (CS) architecture based single connection test case for a Class 2 transport protocol, and a CS architecture based multiplexing test case for the same Class 2 transport protocol.