High quality development of critical systems poses serious challenges. Formal methods have been proposed to address them, but their use in industry is not as wide-spread as originally hoped. We thus propose to use the Unified Modeling Language (UML), the de-facto industry standard specification language, as a notation together with a formally based tool-support for critical systems development.We introduce UML Machines, which is a formal notation designed to reflect properties of the UML execution semantics relevant to criticality requirements. We use it to define a foundation that puts models for the different diagrams into context and gives a precise meaning to mechanisms such as message-passing between objects or components specified in different diagrams, while offering the possibility to analyze criticality requirements.We present tool-support for this approach developed at the TU M?nchen, which facilitates transfer of the methodology to industrial contexts.