TY - GEN
T1 - Verifying UML/OCL models using boolean satisfiability
AU - Soeken, Mathias
AU - Wille, Robert
AU - Kuhlmann, Mirco
AU - Gogolla, Martin
AU - Drechsler, Rolf
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77953100008&partnerID=8YFLogxK
U2 - 10.1109/date.2010.5457017
DO - 10.1109/date.2010.5457017
M3 - Conference contribution
AN - SCOPUS:77953100008
SN - 9783981080162
T3 - Proceedings -Design, Automation and Test in Europe, DATE
SP - 1341
EP - 1344
BT - DATE 10 - Design, Automation and Test in Europe
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - Design, Automation and Test in Europe Conference and Exhibition, DATE 2010
Y2 - 8 March 2010 through 12 March 2010
ER -