Abstract. MBE (Model-Based Engineering) proposes to develop software by taking advantage of models, in contrast to traditional codecentric development approaches. If models play a central role in development, model properties must be formulated and checked early on the modeling level, not late on the implementation level. We discuss how to validate and verify model properties in the context of modeling languages like the UML (Unified Modeling Language) combined with textual restrictions formulated in the OCL (Object Constraint Language). Typical modeling and transformation languages like UML (Unified Modeling Language), EMF (Eclipse Modeling Framework), QVT (Queries, Views, and Transformations) or ATL (Atlan Transformation Language) are complemented by the textual OCL (Object Constraint Language) enriching graphical or textual models with necessary details. Models allow the developer to formulate essential system properties in an implementation- and platform-independent way. Precise ...