Verifying UML/OCL models using Boolean satisfiability

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 codesign. 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.