Nils Przigoda, Robert Wille, Rolf Drechsler,
"Ground Setting Properties for an Efficient Translation of OCL in SMT-based Model Finding"
: International Conference on Model Driven Engineering Languages and Systems (MODELS), 2016
Original Titel:
Ground Setting Properties for an Efficient Translation of OCL in SMT-based Model Finding
Sprache des Titels:
Englisch
Original Buchtitel:
International Conference on Model Driven Engineering Languages and Systems (MODELS)
Original Kurzfassung:
Model Finding is an established method to increase the condence in the correctness of a UML/OCL model, e. g., by
automatically determining valid system states or counterexamples. In the recent past, numerous approaches have been
proposed for this purpose. In order to cope with the underlying complexity, approaches based on satis ability solvers
have been found promising. They require a translation of
all OCL constraints of the model for a corresponding solver.
In this paper, SMT-based model finding is investigated. It
is shown that certain OCL operations are causing huge SMT
formulations which harm the solving process. However, this
is not necessary if a fixed structure of the model can be
assumed. Motivated by this, a new concept called ground
setting properties is introduced which allows for an efficient
translation of OCL into SMT. This concept is illustrated
by means of a running example and compared to existing solutions.
Forschungs-