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

• Type: Conference
• Year: 2010
• Where: DATE
• Authors: Mathias Soeken, Robert Wille, Mirco Kuhlmann, Martin Gogolla, Rolf Drechsler
• Keywords: Actual Verification Task, Complex Software Systems, DATE 2010, Hardware, Verification Tasks