Therefore, a new UML-based modeling technique is presented in this thesis. This modeling technique is used for the specification of reconfigurable systems which integrate behavior from the mechanical, electrical, and from the software engineering domain. To support the model-driven engineering approach, the new modeling approach is seamlessly integrated in an approach for the model-based specification and verification of real-time systems. As standard verification techniques are not feasible for complex systems, the specification of real-time communication protocols, real-time behavior, and reconfiguration is separated. Applying compositional real-time modelchecking and using the separation in combination with refinement relations reduces the effort to ensure that these specifications are not contradictive and that the specified real-time requirements hold.
In order to ensure that the verification results do not just hold for the models, but also for the implementation, a code generator is presented. The applications derived by this code generator integrate implementations of the models from the different engineering domains, guarantee to hold the specified and verified real-time requirements, and provide efficient implementations in spite of complex reconfiguration.