UMLtoCSP

What is UMLtoCSP?

UMLtoCSP is a tool for the automatic verification of UML models annotated with OCL constraints. It can check automatically several correctness properties about the model, such as the satisfiability of the model or the lack of contradictory constraints. The tool supports UML class diagrams only.

The inputs of the tool are an XMI or Ecore file with an UML class diagram and a text file with OCL constraints. After selecting the correctness property to be verified, it translates those inputs into a Constraints Satisfaction Problem (CSP) in the format of the ECLiPSe constraint solver. Solving the CSP leads to an instantiation of the class diagram that proves or disproves the correctness property.

The most relevant features offered by UMLtoCSP to model designers are:

• Fully automatic verification of UML class diagrams with OCL constraints.
• Using the tool does not require any knowledge of the underlying formalism.
• Results are shown graphically as object diagrams.

You can find more information about UMLtoCSP in the papers at ASE'2007 [ PDF ], MODEVVA'2008 [ PDF ] and the Journal of Systems and Software [ PDF ]. A protoype of the tool which adds support for OCL preconditions and postconditions is presented [ here ].

IMPORTANT: New developments for this tool continue within EMFtoCSP, a tool which shares the underlying solver technology but is intregated in the Eclipse IDE. This tools is developed in collaboration with the AtlanMod research group (INRIA, Ecole des Mines de Nantes).

Downloading and installing

In order to execute UMLtoCSP you will need the following applications in your system:

• A Java Runtime Environment version 1.5 or above (Get it here).
• The ECLiPSe Constraint Programming System version 5.10 or above (Get it here). There is an EXE installer for Windows and both RPM and source distributions for Linux.
• The Graph Visualization Package Graphviz (Get it here). There is an EXE installer for Windows and both RPM distributions for Linux. Also, this software is installed by the ECLiPSe installer for Windows.

You can download the UMLtoCSP distribution here:

The tool can be executed by invoking the scripts UMLtoCSP.bat (Windows systems) or UMLtoCSP.sh (Linux systems). The first time the tool is executed, the Configure menu should be used to select the paths where the external tools ECLiPSe and GraphViz have been installed. UMLtoCSP will make an educated guess on the location of those tools which will be correct in most Windows systems, but we recommend that the user checks the configuration before attempting to verify any model.

Screenshots

Click on a screenshot to enlarge the picture.

Main window	Selecting parameters for verification	Choosing properties to be verified

Object diagram computed by the tool

Using UMLtoCSP

Using UMLtoCSP to verify a UML/OCL model is simple. You just need to follow these steps:

• Step 1: Load the model.

  A model consists of two files: the XMI files with the UML class diagram and an text file with OCL constraints. If you do not choose a file for the OCL constraints, UMLtoCSP will assume the class diagram has no OCL constraints, i.e. it only has to check aspects like multiplicities of associations and inheritance.

• Step 2: Choose the property to be verified.

  The designer should choose the property of the model that it wants to verify. By default, UMLtoCSP assumes that the property to be verified is strong satisfiability: checking that it is possible to build an instantiation of the model where the population of each class is not empty.

• Step 3 (optional): Choose the limits of the search.

  UMLtoCSP will try to find an instantiation of the model that can be used to prove the property selected by the designer. As the number of instantiations of a model may be infinite, it will restrict its search to a bounded set of instantiations. The limits of the search are defined by establishing bounds on the number of objects in each class, the number of links of each association and the possible values of each attribute. The designer may make the analysis more efficient by defining tight bounds or more complete by defining wider bounds. Typically, the designer will use the default values chosen by UMLtoCSP.

• Step 4: Verify the property.

  The verification in UMLtoCSP is completely automatic: just press a button and wait for the result! The result is shown graphically as an object diagram that you can save as a PNG image.

Some useful tips:

• You can have several UML/OCL models opened simultaneously.
• The performance of verification depends on the limits of the search. If your verification is too slow, try analyzing the model with tighter bounds.
• UMLtoCSP is performing bounded verification: if it finds an instance, it will prove the property. However, being unable to find an instance does not disprove the property in general, only within the search space.
• If you want to create and load your own models, we recommend using the XMI export in ArgoUML or Gentleware's "Poseidon for UML 3.0" (there is a free community edition). If you use Poseidon for UML 4.0 you must first process the exported XMI file with the XSLT provided in [ XML file ]. Make sure your model's XMI file does not contain diagram data (untag the corresponding option when saving XMI file)

Examples

• Papers and Researchers
  • UML class diagram [ XMI file, PDF image ].
  • OCL constraints [ text file ].
  • CSP translation [ ZIP file ].
• E-commerce (example with OCL operations) [ here ]

Links

• EMFtoCSP
• Dresden OCL tool-kit
• ECLiPSe Constraint Programming System
• The Java Programming Language
• Apache Ant