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 tech- niques, especially those based on formal methods, are more and more used for enhancing traditional System Engineer- ing 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 confor- mance 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 sub- set 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.