Logo to CSP (UOST)

Welcome to our website UML to CSP (UML/OCL Slicing Technique) (UOST)

About UMLtoCSP (UOST)?

UMLtoCSP (UOST) with UML/OCL slicing technique is a tool for automatic verification of UML class diagrams annotated with OCL constraints. The tool can verify complex UML/OCL class diagrams in order to improve the efficiency of the verification process. It can check automatically several correctness properties about the class diagram, such as the satisfiability of the class diagram with respect to non-disjoint slicing method. UMLtoUSP (UOST) is limited to UML class diagrams.

The input of the tool an XMI with a UML class diagram and a text file with OCL constraints. It will break the class diagram into several independent submodels with respect to the slicing criteria. After selecting the correctness property to be verified, it translates all slices 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.

UMLtoCSP (UOST) has the following features:

bullet Fully automatic verification of submodels of an original UML class diagram with OCL constraints.

bullet Verification of complex UML/OCL class diagrams.

bullet No knowledge required for transformation or formalism.

bullet Detection of the OCL constraints in case of unsatisfiable UML class diagram.

bullet The output is shown in the form of an object diagram for each slice.

The details of UML/OCL Slicing Technique (UOST) can be found in ASE 2012 paper [ PDF ] and SAM 2011 [ PDF ].

Valid XHTML 1.0 Transitional