Skip to main content
Article
Automatic Test Generation From Statecharts Using Model Checking
Technical Reports (CIS)
  • Hyoung Seok Hong, University of Pennsylvania
  • Insup Lee, University of Pennsylvania
  • Oleg Sokolsky, University of Pennsylvania
Document Type
Technical Report
Date of this Version
1-1-2001
Comments
University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-CIS-01-07.
Abstract

This paper describes a method for automatic generation of tests from specifications written in Statecharts. These tests are to be applied to an implementation to validate the consistency of the implementation with respect to the specification. For test coverage, we adapt the notions of control-flow coverage and data-flow coverage used traditionally in software testing to Statecharts. In particular, we redefine these notions for Statecharts and formulate test generation problem as finding a counterexample during the model checking of a Statecharts specification. The ability to generate a counterexample allows test generation to be automatic.

To illustrate our approach, we show how to translate Statecharts to SMV, after defining the semantics of Statecharts using Kripke structures. We, then, describe how to formulate various test coverage criteria in CTL, and show how the SMV model checker can be used to generate only executable tests.

Keywords
  • software testing and analysis,
  • specification-based testing,
  • test generation,
  • control and data flow analysis,
  • Statecharts,
  • model checking,
  • CTL,
  • SMV
Citation Information
Hyoung Seok Hong, Insup Lee and Oleg Sokolsky. "Automatic Test Generation From Statecharts Using Model Checking" (2001)
Available at: http://works.bepress.com/sokolsky/4/