On the verification of UML/OCL class diagrams using constraint programming

• We describe a bounded verification technique to analyze software models described in the UML/OCL notations.
• The approach relies on constraint programming to compute satisfying instances.
• This method can deal with complex invariants which may include numerical constraints.

Assessment of the correctness of software models is a key issue to ensure the quality of the final application. To this end, this paper presents an automatic method for the verification of UML class diagrams extended with OCL constraints. Our method checks compliance of the diagram with respect to several correctness properties including weak and strong satisfiability or absence of constraint redundancies among others. The method works by translating the UML/OCL model into a Constraint Satisfaction Problem (CSP) that is evaluated using state-of-the-art constraint solvers to determine the correctness of the initial model. Our approach is particularly relevant to current MDA and MDD methods where software models are the primary artifacts of the development process and the basis for the (semi-)automatic code-generation of the final application.