Executable EFSM-based data flow and control flow protocol test sequence generation using reachability analysis

This paper presents an executable Extended-Finite-State-Machine (EFSM)-based protocol test sequence generation method with specified variable bound. The proposed method overlaps data flow and control flow tests. In the data flow part, the transition paths that contain definition uses and output uses of variables in the protocol specifications need to be detected and tested. An executable data flow test path, which is called an EDO-path, contains two parts: (1) a switching transition sequence that directs to a transition T containing a definition use of a variable V, and (2) a transition sequence originated from T, such that its head transition has a definition use of V and its tail transition contains either (i) an output use of V, or (ii) an output use of another variable which is affected by this definition use of V. In the control flow part, each transition must be tested as to whether it conforms to the original specification or not. An executable control flow test path, which is called an EC-path, for a transition T contains (1) a switching sequence that directs to the head state of T, (2) the transition T itself, and (3) the Unique Input/Output sequence of T's tail state, which verifies whether the tail state of T is correct or not. To shorten the length of the total test sequences, the proposed method overlaps the control flow test sequences with the data flow test sequences. That is, a test sequence may combine both control flow and data flow tests. The overlap is achieved as follows: when of searching EDO-paths, EC-paths are also searched in the same executable transition exploration sequences. If not all of the EC-paths are overlapped with EDO-paths, the remaining EC-paths are searched individually. Additionally, to provide flexible protocol conformance testing, protocol testers can specify some variable bound for their specific test purposes. That is, protocol testers can run tests they are interested in by specifying the associated variable bound in the protocol specification.