I will present a mapping from OCL (Object Constraint Language) to first-order logic. This mapping allows us to reason on UML models with OCL expressions and check satisfaction of them. Our translation considers the four-value characteristics of OCL and is significantly more comprehensive than previous works. Also, I will present a methodology for the analysis of ActionGUI models. ActionGUI models are composed of three UML based models aimed to describe the data, the security restrictions and the GUI behaviour. ActionGUI toolkit generates automatically code from UML, security and GUI models. The quality of the generated code depends on the quality of the source models. If the models do not specify the system intended behavior, one should not expect the generated system to do so either. Using the principles of the aforementioned result, we develop a methodology to analyze different kind of properties on ActionGUI models. They include checking consistency of the data model and analysis of invariant preservation on the GUI model. The methodology was implemented using SMT solvers and automatic theorem provers as back ends.