A methodology and a framework for model-based testing

In this paper we will present a survey on the test case generation process and tools we are currently developing. It will reflect the new ideas that we're pursuing while keeping in mind our previous work on formal specification languages and theory of test case generation. The model based test case generation method we propose is based on a subset of the Unified Modelling Language (UML) and the Object Constraint Language (OCL). It uses UML diagrams in what concerns the conceptual point of view and, in addition, OCL expressions for the system's behavioral description. The research builds on past experience of the group while generating test cases starting from a model of the SUT (System Under Test) described in the CO-OPN formalism - formal language for system specification that acts as an intermediary format between the model and the tests. Our method makes use of well known techniques such as symbolic execution by means of a logic resolution engine (i.e. Prolog) for state space exploration of the SUT.