This short contribution demonstrates central options in the tool USE (Uml-based Speci cation Environment) for exploring UML models within software development. It particularly uses so-called classifying OCL terms for building validation and veri cation scenarios and for completing partial models. The contribution demonstrates the tool's options with an example: statecharts together with a simple syntax model and a model for capturing nite fractions of the statechart semantics.
In this paper, we demonstrate the options available in the tool USE [
The structure of the rest of this paper is as follows. Section 2 presents the background work: CTs and the USE model validator completion capabilities. Section 3 shows how a system can be tested with cts and object model completion. Section 4 compares our work to similar related proposals. Finally, Sect. 5 concludes the paper.
Our running example is shown in Fig. 1 with a class model and names of needed OCL invariants. The model serves to describe the syntax of statecharts (left part of the class model) and a semantics for statecharts in terms of a nite number of traces (right part). The top left object model in Fig. 2 shows on the left an example for a statechart and on the right an example trace. One could also say that the left side represents design time elements and the right side runtime items. The OCL invariants for the syntax part require unique state names, existence of a single initial and a single nal state, deterministic transitions, and each state to lie between the initial and the nal state. The OCL invariants for the semantics part require each trace to be a cyclefree string of pearls (TraceNode objects linked together looking like a string of pearls), to be connected to the initial state and to show events corresponding to the transition events. Our view on the model is that we have speci ed syntax and semantics of a particular statechart language. Our tool allows the developer to systematically explore the model by building test cases in form of object models and thereby to validate and verify model properties and get con dence into the model. 2.2
Usual approaches to generate object models from a metamodel explore the state space looking for di erent solutions. The problem is that many of these solutions are in fact very similar, only incorporating small changes in the values of attributes and hence \equivalent" from a conceptual or structural point of view.
Classifying terms (CTs) [
Fig. 2. Four di erent object models constructed with classifying terms. values, selecting one canonical representative object model. Hence, the resulting set of object models is composed from one object model per equivalence class, and therefore they represent signi cantly di erent test cases. Besides, they partition the full input space. For example, the following classifying terms could be de ned for our metamodel. context State inv i n i t i a l E q F i n a l : let INI=State . allInstances >any ( s j s . i s I ni t i a l=true ) in let FIN=State . allInstances >any ( s j s . isFinal=true ) in
INI=FIN -- i n v a r i a n t s o n e I n i t i a l and oneFinal give d e t e r m i n a t e n e s s context T r a n s i t i o n inv t w o T h r e e O r F o u r E v e n t s : let n u m E ve n t s=T r a n s i t i o n . allInstances > -- collect yields Bag collect ( t j t . event ) >asSet ( ) >size ( ) in n u m Ev e n t s=2 or n u m Ev e n t s=3 or n u mE v e n t s=4
Each of these two CTs may be true or false. Together, they de ne four equivalence classes. First, we want to distinguish between statecharts in which the initial and the nal state coincide, and others with di erent initial and nal states. Second, we want to have some sample models in which there are 2, 3 or 4 events, and other models in which there could be less than 2 or more than 4 events. The model validator, which is the tool in charge of exploring the search space and generating object models, will simply return one representative of each of the four equivalence classes. Note that CTs do not always pretend to generate models that are representative of the complete metamodel, they might be used to generate models that contain interesting features w.r.t. concrete scenarios of interest to the modeller, and which are only relevant in a sub-part of the given speci cation. They are also useful for nding object models that should not happen in theory, i.e. counterexamples for our speci cation. 2.3
Object models are automatically generated from a set of CTs by the USE model
validator, which builds and inspects object models and selects one representative
for each equivalence class. For this, as described in [
The validator has to be given a so-called `con guration' that determines how the classes, associations, data types and attributes are populated. In particular, for every class a mandatory upper bound for the number of objects must be stated. Both the USE tool and the model validator plugin are available for download from http://sourceforge.net/projects/useocl/. 3
In order to illustrate our proposal, let us consider the object models shown in Fig. 2. These structurally di erent object models have been automatically generated by using 4 boolean-valued CTs (and a con guration xing attribute values, links, and lower and upper bounds for the number of objects in a class): context State inv t w o St a t e s : State . allInstances >size=2 context State inv t h r e e S t a t e s : State . allInstances >size=3 context T r a ce N o d e inv oneTrace : T r ac e N o d e . allInstances >
select ( tn j tn . src >isEmpty ( ) and tn . trg >notEmpty ) >size=1 context T r a ce N o d e inv t w o Tr a c e s : T r a ce N o d e . allInstances > select ( tn j tn . src >isEmpty ( ) and tn . trg >notEmpty ) >size=2 In principle, 24 = 16 equivalence classes are possible. However, this number will not be reached, because, for example, the classifying terms twoStates and threeStates cannot be true at the same time. Figure 2 shows 4 found solutions. Essentially, the upper row shows the solutions with 2 states and the lower row the solutions with 3 states; and the left column displays the solutions having 1 trace and the right column the solutions with 2 traces.
Another important option in USE is to specify an incomplete object model with missing attribute values, objects or links, and to ask the USE model validator to complete the incomplete model into a full model. Fig. 3 shows an example. In the right side of the upper part, two example traces for two Paper objects submitted to a Conference together with an incomplete statechart in the left are shown. In the lower part the result of asking the model validator to complete the object model is pictured. The model validator has found attribute values and link-objects for association classes in order to satisfy all model constraints. Our view is that the full statechart has been automatically deduced from two example traces and an incomplete statechart description. The price we have to pay is that we have to present an exhaustive set of invariants. The full models are available. 4
The USE model validator is based on the transformation [
Exploring the execution space of any non-trivial system is a di cult task. In this paper we have shown how the tool USE can be employed, in conjunction with classifying terms, to specify particular validation and veri cation scenarios, allowing system analysts to look for object models that satisfy certain properties, or their absence. There are several lines of work that we plan to address next. First, we would like to validate our proposal with more examples, in order to gain a better understanding of its advantages and limitations, and to identify di erent contexts of use in which our approach works well and others in which the results are not satisfactory (and why). Second, we plan to improve tool support to further automate all tests, so human intervention is kept to the minimum. Finally, we need to de ne a systematic approach of de ning classifying terms for exploring object models using the outlined ideas.