Abstract
The Unified Modeling Language (UML) is an object-oriented analysis and design language. To support the design of large-scale industrial applications, automated verifying the correctness of UML diagrams is necessary. However, existing methods limit automatic verification to only one or two diagrams. In this paper, we present a method of automated reasoning on several UML diagrams, which applies the idea of model checking. First of all, UML diagrams and formal properties of UML diagrams are represented with logic programs. Then the semantics of the logic programs are computed. After that, correctness of the UML diagrams can be determined by checking whether the logic formulas of the properties are true in the semantics.