Model checking of statecharts using automatic white box test generation

This paper describes a model checking technique and tool for UML statecharts based on automatic white box test-generation combined with automatic run-time monitoring of statechart assertions. The white box test generator is an automatically generated JUnit TestCase, which generates sequences of events, conditions, and input data for the system under test (SUT). It generates test sequences while observing the SUT´s state, knowing the input events, conditions, and data objects that potentially affect the SUT´s next state. The white box tester then chooses one of those events, conditions, and data objects, and fires the SUT, which in turn fires an embedded assertion for run-time monitoring. This combination of white box testing with assertion monitoring constitutes automatic model checking. The white-box test-generator is also specification based in that the white box can be specified to be requirement assertions