Publisher's Synopsis
The Unified Modeling Language (UML) and the model-driven engineering (MDE) approach became standard in software engineering. The recent development in the design of mechatronic systems, which combine technologies from mechanical and electrical engineering as well as from software engineering, applies increasingly UML and MDE. Nowadays, new trends in mechatronics like the integration of self-optimization lead to reconfigurating systems which require advanced engineering techniques: Reconfigurating systems change their structure at runtime. This includes the exchange of single modules and restructuring of the communication connections. Even the application of existing UML-based modeling techniques for such systems leads to complex models which are difficult to handle and hard to analyze.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.
