Model driven development with mechatronic UML

We address these challenges by the model-driven mechatronic UML development approach which combines domain specific modeling and refinement techniques with verification based on compositional model checking. The approach suggests modeling the software by using a refined UML 2.0 component model including the detailed definition of ports, connectors, and patterns. We further refine the component model to define a proper integration between discrete and continuous control such that the reconfiguration of hierarchical component systems can be described in a modular way. Compositional model checking is based on a domain specific decomposition of the system specification into individually checkable components based on a common pre-defined architectural model. As a basis for formal verification, a formal semantic definition of the concepts taken from UML 2.0 is given. For the scope of this presentation, this is particularly done for our notion of so-called real-time statecharts. Besides supporting compositional verification, the approach supports checking consistency between different parts of a systems specification by a syntax check. This check is based on giving a formal definition of consistency.