My work on formal verification is mainly done in the context of my GRES research group . In the context of this group we have developed the UMLtoCSP tool. 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. Currently, the tool works on UML class diagrams only. The inputs of the tool are an XMI 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.

We have also proposed a set of challenges to make the verification of UML/OCL models feasible in practice in this paper .