Patent ID: 8370808

Claim:
An apparatus for generating a test case of a system to be checked, comprising: a first memory configured to store a state-transition system including a plurality of states and a first transition between two of the plurality of states in the system, each state being represented by a plurality of internal variables, the first transition representing a state-change based on an external event occurred into the system; a second memory configured to store a plurality of requirement items each including a precondition and a postcondition in correspondence with the external event, the precondition describing a state of the system before occurrence of the external event, the postcondition describing a state of the system after occurrence of the external event; a state predicate extraction unit configured to select m (m: an integral number equal to or larger than one) requirement items from the second memory, and extract the precondition and the postcondition from the m requirement items; a state map generation unit configured to generate a state map to map an indicated state onto truth values of the precondition and the postcondition; a state equivalence relation definition unit configured to acquire a plurality of mapped values by mapping each of the plurality of states by the state map, and generate a plurality of groups each including states having the same mapped value; a quotient state-transition system generation unit configured to select two groups from the plurality of groups, set a second transition from one of the two groups to the other of the two groups when the first transition from one state included in the one to one state included in the other exists in the state-transition system, and generate a quotient state-transition system including a plurality of second transitions among the plurality of groups by repeating selection of the two groups and set of the second transition; a representative transition path generation unit configured to generate a representative transition path as a sequence of each second transition by tracing the plurality of second transitions from a predetermined group of the plurality of groups; a transition path generation unit configured to select the second transition from the representative transition path in order of the tracing, specify the first transition of which an origin state is same as one state of an origin group of the selected second transition and a destination state of a previous first transition specified, a destination state is same as one state of a destination group of the selected second transition, and generate a test case including a sequence of each first transition specified; and an output unit configured to output the test case.