From UML and OCL to relational logic and back

Abstract

Languages like UML and OCL are used to precisely model systems. Complex UML and OCL models therefore represent a crucial part of model-driven development, as they formally specify the main system properties. Consequently, creating complete and correct models is a critical concern. For this purpose, we provide a lightweight model validation method based on efficient SAT solving techniques. In this paper, we present a transformation from UML class diagram and OCL concepts into relational logic. Relational logic in turn represents the source for advanced SAT-based model instance finders like Kodkod. This paper focuses on a natural transformation approach which aims to exploit the features of relational logic as directly as possible through straitening the handling of main UML and OCL features. This approach allows us to explicitly benefit from the efficient handling of relational logic in Kodkod and to interpret found results backwards in terms of UML and OCL. © 2012 Springer-Verlag.