Formal test-case generation for UML statecharts

The Unified Modeling Language has been introduced as a notation for modeling and reasoning about large and complex systems, and their design, across a wide range of application domains. System modeling 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 labeled by input/output-pairs (IOLTSs). IOLTSs provide a suitable semantic model for a behavioral 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.