# UCLAONT: Ontology-Based UML Class Models Verification Tool updates
## 1 Introduction
However, both of them only verify the initial level of syntax weaknesses and do not concern the model's semantic correctness. Semantic correctness concerns the constraints which are specified in the model graphically such as associations, dependencies, and generalizations, or textually defined through constraint language such as Object Constraint Language (OCL). The most fundamental semantic correctness property of the UML class model is satisfiability [19]. Other important correctness properties which are verified and come under the umbrella of satisfiability are strong satisfiability, weak satisfiability, and class liveliness [22]. Strong satisfiability checks whether a model can instantiate successfully in which one instance of each element successfully populates. Weak satisfiability checks whether at least one or more elements of the model can be instantiated successfully. Class liveliness checks whether a class can populate successfully. The problem addressed in this work is twofold and can be stated as follows:  
Firstly, current UML class model verification methods are sufficiently good to check correctness. However, they do not focus on some fundamental class model elements such as dependency relationships and XOR constraints. With few exceptions in which the XOR constraint is indirectly supported by some existing methods through OCL, however, OCL has some limitations. For example, UML specification does not restrict constraint language, and according to the UML specification, constraints can be defined through formal languages, informal languages (JAVA, C#), and natural language [23]. Most of the Computer-Aided Software Engineering (CASE) tools do not support OCL or provide limited support because commercial CASE tools do not see a large market of OCL [24]. Secondly, the problem faced by the current verification methods is scalability due to its high computational complexity [13; 25]. When they deal with large and complex models, they consume enormous computational resources and time [14]. In [19], authors also identified different research directions for future UML class diagram verification methods, in which one is search space reduction for dealing with scalability issues. Therefore, there is a need for UML class model verification methods that efficiently verify large and complex models within a reasonable time and with minimum computational resources. Previously, we proposed ontology-based transformation and verification of UML class model unsupported elements, that is, XOR constraints and dependency relationships. These transformations map XOR and dependency relationships to an ontology for verification of various correctness properties such as satisfiability, consistency, and consequences. The proposed method verifies a large UML class model in an acceptable time [26]. In this paper, we extend our work in multiple directions. Firstly, it presents the complete transformation mechanism of UML's XMI to ontology. Secondly, it demonstrates the implementation details (Pseudocode) of the verification method proposed in the previous work. Finally, it presents the complete transformation and the verification model. Furthermore, this paper explores the various components of the tool and algorithms which have been used in the Ontology-Based Verification method. Additionally, it shows the performance of the tool in the real world for large and complex UML class models. In total, this paper presents the software implementation of our previously published works [26; 27; 28; 29]. The rest of the paper is structured as follows. Section 2 presents related work. Section 3 focuses on the running example along with the details of ontology-based finite satisfiability. Section 4 explores the tool architecture with all details of transformation rules. Section 5 describes the experimental results measuring verification time as compared to other tools. Finally, Section 6 provides the conclusions and future directions.