Research on formal test execution methods is an important phase in the activity of formal protocol conformance testing. This paper proposes a formal test execution approach based on test notation language TTCN s operational semantics and described it by using labeled transition system, and also discusses an implementation of this method. This formal approach is very suitable for the construction of general protocol testing system, and can be an effective way for automatic test suite verification.