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
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:
|UMLtoCSP - Latest release|
UMLtoCSP.ZIP [ ZIP file ]
|Version date:||Jun 26, 2009|
|What's new?:||Ecore (EMF) input model support, Improvements regarding generalizations, bug fixes, performance improvements |
|Platforms:||Windows and Linux|
The tool can be executed by invoking the scripts
UMLtoCSP.bat (Windows systems) or
(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.
Click on a screenshot to enlarge the picture.
||Selecting parameters for verification
||Choosing properties to be verified
|Object diagram computed by the tool
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
- 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)
- Papers and Researchers
- E-commerce (example with OCL operations) [ here ]