We present in this paper a technique and a tool for validating operational UML models by simulation and verification of dynamic properties. With respect to language coverage, our approach takes into consideration most of the structural and behavioral characteristics of classes and their interplay. We tackle issues like the combination of operations, state machines, inheritance and polymorphism, with a particular run-to-completion and concurrency semantics. This is an important point, as many previous approaches applying model checking to UML put limiting conditions on the models. The UML dialect considered here also includes a set of extensions for expressing timing, which were defined in detail in [...]. For writing properties about models, we introduce UML observer objects. Observers are both easy to use -- they reuse existing concepts of UML, and powerful --- they are equivalent to linear temporal logic. Our approach is implemented by a tool built on top of an XMI repository. The tool is connected to several commercial and non-commercial UML editors, and to other model checking tools.