Using the NuSMV Model Checker for Test Generation from Statecharts

Testing is essential to ensure the dependability of software systems. This paper proposes an automatic test case generation method using the NuSMV model checker. We consider state-transition testing based on Statechart specifications. Given a Statechart specification, our proposed method can automatically generate test cases that cover all states or all transitions in the Statechart. Finding such test cases requires traversing the state space of the system under test. In practice, however, the state space can often be very large and thus a fast search method is required. To this end our method makes full use of NuSMV. We devise a technique for modeling and analyzing Statecharts so that test cases can be extracted from the counterexamples produced by the model checker. The feasibility of our method is demonstrated through case studies.