# UCLAONT: Ontology-Based UML Class Models Verification Tool updates
## 1 Introduction  
A model is an abstract representation that is used to analyze and comprehend a system [1]. In the engineering world, models are used in almost every discipline, such as the house map in civil engineering and circuit diagram in electronic engineering. These models are used to understand the characteristics of the system [2]. In software engineering, design models play a vital role in software development. In modern software engineering methodologies, they are used to elicit requirements, design the system, and generate the code. Software design models are a formal description of the structures and behaviors of the system. The discourse is the complete software design, including functionality, architecture, collaboration, user interfaces, and interaction with other software [3]. In software engineering, designing a model before the implementation is very beneficial. It provides an understandable view of the system and improves communication among all stakeholders. Furthermore, the software design model provides early identification of incompleteness and inconsistencies in the underdeveloped system with the help of model verification techniques [4; 5]. Current software design modeling techniques such as Unified Modelling Language (UML) and Systems Modeling Language (SysML) are robust and cover all aspects of software development. However, they do not have a formal foundation. Therefore, verification of the model is not possible in them. On the other side, formal modeling methods provide the capability of analysis. A formal model mathematically represents the software specification and provides an automated reasoning facility [6; 7; 8]. They eliminate ambiguities, design faults and improve system reliability [9]. However, they are complex andinspired by mathematics [10]. UML is a modeling language that is especially involved in the specification and visualization of the object-oriented system. Initially, Rational software developed the UML, but now Object Modeling Groups (OMG) managing it [11]. In the UML, an underdeveloped software system is represented by a set of different models, and each model focuses on a different facet of the software. The UML class model is the most essential element of UML. According to a survey presented in [12], it is the most frequently used UML model. It is also a vital ingredient of the MDE process [13; 14; 15]. The main elements of a class model are classes and different types of relationships such as dependency, association, and generalization [16]. Association and generalization are also dependency relationships; however, they have specific semantics [16]. These three relationships (dependency, association, generalization) are the basic building block of UML and object-oriented modeling [16]. In modern software development methodology like Model-Driven Engineering (MDE), the software design model is considered a nucleus of all development activities and is recognized as a core element rather than a traditional programming language code [3; 4; 17; 18]. In Model-Driven Software Engineering, the programming language code is produced from the design model automatically, and defects of the model can implicitly transfer in the programming code, which is harder to determine and repair. Model verification is a feasible solution to this problem. Model verification ensures that the model will be built without errors. It makes sure that the model must have some important correctness features such as satisfiability and consistency [19]. Model is considered incorrect when it does not satisfy any correctness features, and when it satisfies all correctness features, it is considered correct [19]. Satisfiability, consistency, and well-formedness are the most fundamental correctness proprieties [19; 20; 21]. The consistency verifies whether the model elements are consistent with the declaration, whereas well-formedness verifies whether a model is a valid instance of its meta-model [19; 20].