Modeling and verification of cooperative self-adaptive mechatronic systems

The advanced mechatronic systems of the next generation are expected to behave more intelligently than today's systems by building communities of autonomous agents which exploit local and global networking to enhance their functionality. Such mechatronic systems will therefore include dynamic structural adaptation at the network level and complex real-time coordination protocols to adjust, their behavior to the changing system goals leading to cooperative self-adaptation in a safe and coordinated manner. In this paper the Mechatronic UML approach and its concepts for compositional modeling and verification of crucial safety properties for cooperative self-adaptive mechatronic systems are outlined. Based on former results for the compositional verification of the real-time coordination and safe rule-based dynamic structural adaptation, we present in this paper a systematic compositional verification scheme which permits to verify the safety of real-time systems with compositional adaptation and an a priori unbounded number of structural configurations.