Verifying UML/OCL models using Boolean satisfiability

TLDR

UML modeling is essential for complex software and emerging hardware design, and time‑to‑market pressures demand first‑time‑right requirements. The paper proposes using Boolean satisfiability to verify UML/OCL models. The method encodes UML model states, OCL constraints, and verification tasks into SAT and solves them with an off‑the‑shelf solver. Experiments demonstrate that the approach solves verification tasks faster than prior methods while supporting many UML/OCL constructs.

Abstract

Nowadays, modeling languages like UML are essential in the design of complex software systems and also start to enter the domain of hardware and hardware/software co-design. Due to shortening time-to-market demands, first time right requirements have thereby to be satisfied. In this paper, we propose an approach that makes use of Boolean satisfiability for verifying UML/OCL models. We describe how the respective components of a verification problem, namely system states of a UML model, OCL constraints, and the actual verification task, can be encoded and afterwards automatically solved using an off-the-shelf SAT solver. Experiments show that our approach can solve verification tasks significantly faster than previous methods while still supporting a large variety of UML/OCL constructs.