Test case generation for UML statecharts

We describe an approach to automatically generate test cases from object-oriented statecharts as they are used in the UML and supported by development tools such as I-Logics Rhapsody. This work contributes in three respects to using statecharts for specifying and verifying systems. First, it concretizes previously proposed semantics of statecharts by instantiating the abstract data type for the event management and analyzes the resulting specific properties. Second, building on a previously defined conformance relation it discusses two interpretations of stuttering. Third, it introduces a compact data structure for representing the statechart semantics that allows for efficient generation of test cases and easily supports both interpretations of stuttering.