Formal test-case generation for UML statecharts

The unified modelling language has been introduced as a notation for modelling and reasoning about large and complex systems, and their design, across a wide range of application domains. System modelling and analysis techniques, especially those based on formal methods, are more and more used for enhancing traditional system engineering techniques for improving system quality. In particular this holds for model-based formal test case derivation using formal conformance testing. The contribution of the present paper is to provide a solid mathematical basis for conformance testing and automatic test case generation for UML statecharts (UMLSCs). We propose a formal conformance-testing relation for input-enabled transition systems with transitions labelled by input/output-pairs (IOLTSs). IOLTSs provide a suitable semantic model for a behavioural subset of UMLSCs. We also provide an algorithm which, for a UMLSC specification and the alphabet of implementations, generates a test suite. The algorithm is proven exhaustive and sound w.r.t. the conformance relation.