A formal description of an implementation under test (IUT), such as its VHDL behavior description, is required to automatically generate feasible test sequences for the IUT. Although finite-state machines (FSMs) can be used to describe the control structures of communication protocols, the data portion can only be modeled by extended finite-state machines (EFSMs). However, infeasible paths due to the conflicts among the condition and action variables of EFSMs complicate the test generation process. We introduce a method enabling the automatic generation of realizable test sequences from a class of EFSMs. Algorithms to detect and eliminate conflicts caused by the interdependences among the variables of a class of EFSM models are presented. After all conflicts are eliminated from the EFSM graph, the existing FSM-based automated test generation methods can be used to generate feasible test sequences. Recently, these algorithms have been implemented as a software package called INDEEL. This methodology is applied to generate feasible tests for protocols such as ACA and MIL-STD 188-220. Current applications include IETF protocols and ASAP.

We present a new model for testing real-time protocols with multiple timers, which captures complex timing dependencies by using simple linear expressions involving timer-related variables. This new modeling technique, combined with the algorithms to eliminate inconsistencies, allows generation of feasible test sequences without compromising their fault coverage. The model is specifically designed for testing to avoid performing full reachability analysis, and to control the growth of the number of test scenarios. Based on extended finite state machines, it is applicable to languages such as SDL, VHDL, and Estelle. The technique models a realistic testing framework in which each I/O exchange takes a certain time to realize and timers can be arbitrarily started or stopped. A software tool implementing this technique is used to generate test cases for the US Army wireless standard MIL-STD 188-220.