A Query-based Approach for Verifying UML Class Diagrams with OCL Invariants

Verifying whether a UML class diagram is consistent involves finding valid instances that provably meet its constraints defined in Object Constraint Language (OCL). Recent studies have shown that many existing tools and techniques not only can find valid instances but also pinpoint the conflicts among the OCL constraints. However, they do not scale well and are often unable to locate the conflicts when the number of OCL constraints significantly increases. In this paper, we present a novel approach that is capable of verifying UML class diagrams with a large number of OCL constraints. Our approach has two distinct features: (1) it provides a query language that allows users to choose parts of a UML class diagram to be verified. (2) a new algorithm that can handle an extreme size of OCL invariants via concurrent verification. We have implemented a new automated tool called: QMaxUSE. The evaluation results suggest that QMaxUSE has the potential to be adapted by industry and offers up to 30x efficiency improvement in verifying UML class diagrams with a large number of OCL constraints.