# UCLAONT: Ontology-Based UML Class Models Verification Tool updates
## 2 Related Work
[47] proposed an ontology-based technique for transformation and verification of business process model. This work divided the verification task into two steps. In the first step, different model elements are transformed into the ontology, and constraints of the model are represented through the rules. In the second step, the ontology model and rules are tested through the built-in reasoner. [PERSON] et al. [48] proposed the transformation of software architecture into Web Ontology Language (OWL) and used Semantic Web Rule Language (SWRL) for representing the dynamic communication (constraints). [PERSON] et al. [49] presented an ontology-based transformation and verification of the behavioral model. They also proposed transforming various verification and validation terms, elements, and relationships into the ontology. [PERSON] et al. [31] proposed ontology-based verification of UML behavioral models. The behavior model is divided into static elements specified through ontology and dynamics elements specified by DL-safe rules in this work. [PERSON] et al. [50] proposed the difference between UML and Web Ontology Language (OWL) and presented many common elements such as classes, attributes, and relationships. They also identified the difference between UML and OWL, such as UML having many relationships (association, aggregation, and composition). On the other side, OWL only has an object property. Lastly, they presented that OWL and UML are compatible with each other. [PERSON] et al. [51] presented a different transformation procedure for the class model to ontology. They transformed encapsulation and aggregation/composition into Object Property. [PERSON] et al. [52] proposed a graph-based transformation of the UML class Model into ontology. [PERSON] et al. [53] combined UML with OWL-DL for representing the software model. They integrated the MOF meta-model as the backbone for both UML and OWL. [PERSON] et al. [54] proposed incremental verification of the UML class model. The significant feature of the proposed technique is the use of valid instances of the UML class model as certificates of satisfiability. The proposed technique implemented the UML-based Specification Environment (USE) Tool. [PERSON], [PERSON] et al. [55] present FoCaLiZe development environment for specification and verification of UML class diagram. They generate FoCaLiZe specification of multiple inheritances, dependency template, template binding, and the navigation of OCL contained in the FoCaLiZe specification classes are transformed into species, properties of a class into getter functions, operations into signatures, and OCL constraints into species properties. FoCaLiZe uses Zenon theorem Prover for specification verification. [PERSON] [56] proposed a framework for reasoning on the UML class and the OCL model through Constraint Programming Logic (CPL). They translate the UML class model in constraint satisfaction problems and performed reasoning through the model-finding formula and developed an Eclipse plug-in. the plug-in automatically translates the class diagram into the CPL formula. Current verification methods of the UML class model are capable of checking correctness. However, they do support some fundamental constraints (such as XOR dependencies and XOR). Another problem faced by the existing methods is scalability, due to high computational complexity when dealing with large and complex models verification methods consume enormous computational resources and time. Various existing research works also pointed out different research avenues for future UML class diagram verification methods in which most important is search space reduction for dealing with scalability issues. Therefore, there is a need of UML class model verification methods that efficiently verify large and complex models within a reasonable time and with minimum computational resources.