Checking Unsatisfiability for OCL Constraints

Manuel Clavel, Marina Egea, Miguel Angel García de Dios


In this paper we propose a mapping from a subset of
OCL into first-order logic (FOL) and use this mapping for checking the
unsatisfiability of sets of OCL constraints. Although still
preliminary work, we argue in this paper that our mapping is both
simple, since the resulting FOL sentences closely mirror the
original OCL constraints, and practical, since we can use
automated reasoning tools, such as automated theorem provers and SMT
solvers to automatically check the unsatisfiability of
non-trivial sets of OCL constraints.

Full Text:




Hosted By Universitätsbibliothek TU Berlin.