1. A non-transitory computer-readable medium storing a specification verification program that causes a computer to perform a specification verification of coverage of a requirements specification of a design object against a design specification of the design object, according to operations comprising: acquiring from a use case description as the requirements specification of the design object, one or more anterior, posterior or invariant conditions necessary to be satisfied in connection with execution of each use case; detecting a state from a set of states in a finite state machine model as the design specification of the design object that satisfies one or more of the conditions acquired from the use case description; determining presence or absence of an undetected state in the set of states in accordance with a result of the detection performed in the detecting; and outputting a result of the determining.