A foundation for tool-supported critical systems development with UML

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 defacto 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 Munchen, which facilitates transfer of the methodology to industrial contexts.