UML Validation Toolset's Homepage

Simple Examples

All UML models used in this homepage are edited by Rational Rose Enterprise Edition.

Syntax Check: Let us first take a look at the following example:

In this example, we can see that there are two outgoing transitions from a history state. According to the UML meta-model for history vertices:
```
             ...,...,...,...
[2]. History Vertices can at most have one outgoing transition:
 ((self.kind=#deepHistory) or (self.kind=#shallowHistory)) implies
            (self.outgoing->size<=1)
```
This is an error and when you run this tool you will have the following result:
State Check: When you design a model in the early phase, you give some static structure of a system. In order to check whether some reasonable states are included in the model, you can run this tool. If the states are not included you should redesign the model so as to include these reasonable states. On the other hand, you can check whether some unexpected states are excluded in the model by running this tool. If they are included, you also should redesign the model.
Let us take a look at the following model. In this model, we give constraints associated with classes in the note boxes which connect to the corresponding class because Rational Rose does not support OCL.

Now we want to check whether a state given by an object diagram, shonw in the following, is included in the model:

From the above diagram we can see that the object jay does NOT work in the company ComputerDealer by which the object sellingdesktop he works on is controlled. This violates the constraint inv i5. Then we can run our tool and get the result as follows:
Dynamic Property Check: This tool can not only check the static aspect of a model but verify some properties for a dynamic aspect of a model as well. First let us take a look at a traffic control problem.
"There is a controller that operates the traffic lights at an intersection where a two-way street running north and south intersects a one-way street running east. The control includes three monitors, sensors and sets of the traffic lights (red and green). Each monitor, sensor and set of traffic lights take responsibility for one direction. When a monitor detects a coming traffic, it sends a message to the sensor, which sends a request to the controller. According to the requests from different directions, the controller will send a signal to the corresponding traffic light (either red or green) so as to avoid collisions and make sure no traffic waits at a red light forever.
The controller has three traffic sensor inputs: N_Sense, S_Sense and E_Sense, indicating oncoming traffic in the north, south and east direction respectively. These sensor inputs are triggered by the hardware, monitoring the three different directions. These east, north and south direction's monitors are called E_Monitor, N_Monitor and S_Monitor respectively."
The following is a model for the traffic control system. We give a state machine as follows:

We want to verify whether the model we design satisfy the four properties such as liveness and safety and this is shown as follows:

After running the tool, we have following result:

According to the above result, we find that the safety is not satisfied. After checking the counterexample we know that when a south light turns off at the same time the north light turns on, the lock variable NS_Lock is set to 0, indicating that both north and south traffic lights turn off. Because the lock switches off, the east light turns on when east traffic is coming. This violates the safety property. We redesign our model as follows.

The following is the result for the new model and all properties are satisfied in this new model.

Last change: 19.05.2001 by (wwshen@eecs.umich.edu)