Abstract
Software models are core artifacts in model driven engineering (MDE) and processable by computer. They are automatically transformed into other models and in MDE, programming code is also produced by the models. The automatic transformation provides a systematic reuse of existing artifacts. However, sometimes models are developed with defects and the defects can implicitly shift into the code, which may be difficult to discover and repair. A promising solution to this problem is model verification. UML class model is a key ingredient of MDE. However, UML only offers graphical components without the support of reasoning, due to lack of the formal foundation. Therefore, the verification of formal properties, such as consistency and finite satisfiability is not possible in UML. This paper proposes an ontology-based optimized verification method for important correctness property "finite satisfiability" of UML class model.