Automatic Test Generation From Statecharts Using Model Checking

Abstract

Abstract This paper discusses the application of model checking to test generation from statecharts. We consider a family of coverage criteria based on the control flow and data flow of statecharts and formulate the problem of test generation as finding counterexamples during the model checking of statecharts. The ability of model checkers to construct counterexamples allows test generation to be automatic. To illustrate our approach, we use the temporal logic CTL and its symbolic model checker SMV. We describe how to translate statecharts to inputs to SMV after defining the semantics of statecharts in terms of Kripke structures. We, then, describe how to express various coverage criteria in CTL and show how SMV can be used to generate only executable tests. 1 Introduction This paper addresses the problem of test generation from statecharts [12] that have been widely used for specifying reactive systems. Statecharts can be regarded as extended finite state machines (EFSM) that support the hierarchical and concurrent structure on states and the communication mechanism through event broadcasting. Among several variants of statecharts considered in the literature [2], we concentrate on the STATEMATE semantics for statecharts [13]. Our approach, however, can be immediately applied to other variants of statecharts semantics, for example, the UML statecharts [24]. A statechart specification typically allows an infinite number of executions and hence exhaustive testing is impossible, which requires all the possible executions be performed. The common testing practice is to construct a test suite, that is, a finite set of test sequences according to certain coverage criteria. For test coverage, we adapt the notions of control flow and data flow coverage used traditionally in software and protocol testing to statecharts. For test generation, we illustrate our approach using the temporal logic CTL [8] and its symbolic model checker SMV [21] to statecharts.