Modular verification of safe online-reconfiguration for proactive components in mechatronic uml

Abstract. While traditionally the environment considered by an autonomous mechatronic systems only consist of the measurable, surrounding physical world, today advanced mechatronic systems also include the context established by the information technology. This trend makes mechatronic systems possible which consist of cooperating agents which optimize the system behavior by adjusting their local behavior and cooperation structure to better serve their current goals depending on the experienced mechanical and information environment. The MECHATRONIC UML approach enables the component-wise development of such self-optimizing mechatronic systems by providing a notion for hybrid com-ponents and support for modular verification of the safe online-reconfiguration. In this paper, we present an extension to the formerly presented solution which overcomes the restriction that only purely reactive behavior with restricted time constraints can be verified. We present how model checking can be employed to also verify the safe modular reconfiguration for systems which include compo-nents with complex time constraints and proactive behavior.