Titelaufnahme

Selbstadaptive mechatronische Systeme passen ihr Verhalten über die Rekonfiguration ihrer Softwarearchitektur zur Laufzeit automatisch an eine sich verändernde Umwelt an. Dies ermöglicht insbesondere die Bildung von sogenannten „Systems-of-Systems“ zur Laufzeit, in denen mehrere eigenständige Systeme unter Verwendung nachrichtenbasierter Kommunikationsprotokolle miteinander kollaborieren. Dabei müssen die einzelnen Systeme in der Regel harten Echtzeitanforderungen genügen und sind häufig sicherheitskritisch, d.h. jegliche Fehler im funktionalen oder zeitlichen Verhalten können Menschenleben gefährden. Die besondere Kritikalität dieser Systeme bedingt, dass eine Rekonfiguration der Softwarearchitektur nicht zu einem gefährdenden Verhalten oder einer Verletzung der Echtzeitanforderungen führt. Durch die Anwendung testbasierter Verfahren alleine kann die Korrektheit und damit auch die Sicherheit des mechatronischen Systems nicht garantiert werden. Existierende Ansätze für eine modellgetriebene Entwicklung und Analyse mechatronischer Systeme ermöglichen entweder die Analyse von Echtzeitanforderungen oder die Analyse von Rekonfigurationen der Softwarearchitektur zur Laufzeit jedoch nicht beides. Im Rahmen dieser Arbeit wird eine Kombination aus konstruktiven und analytischen Verfahren vorgestellt. Sie kann von Softwareentwicklern im Rahmen einer modellgetriebenen Softwareentwicklungsmethode eingesetzt werden, um die Korrektheit der Software eines selbstadaptiven mechatronischen Systems zu verifizieren. Die Neuartigkeit des vorgestellten Konzepts liegt in der gezielten Kombination formaler Verifikationsverfahren mit simulations-basierten Testverfahren mit dem Ziel, einen skalierbaren Ansatz für die Analyse der Software zu erhalten. Die Beiträge der Arbeit wurden auf Basis des RailCab Systems und zweier Fallstudien evaluiert.

Self-adaptive mechatronic systems automatically adapt their behavior to a changing environment by reconfiguring their software architecture at runtime. In particular, this includes to dynamically form systems of systems at runtime, where several systems collaborate with each other using message-based communication protocols. Often, these systems are safety-critical and need to satisfy hard real-time constraints, i.e., any (timing) error in their behavior may put lives at risk. As a consequence, the software of a mechatronic system needs to meet high quality standards. In particular, it needs to be guaranteed that reconfigurations of the software architecture do not lead to an unsafe behavior or a violation of the real-time constraints. Testing alone cannot prove the correctness and thereby the safety of the mechatronic system. Existing approaches for model-driven development and analysis of mechatronic systems either provide support for analyzing real-time constraints or for analyzing reconfigurations of the software architecture, but none of the existing approaches supports both. In this thesis, we present a combination of constructive and analytical techniques that can be used by software engineers as part of a model-driven software engineering method for assuring the correctness of the software of a self-adaptive mechatronic system. As a key novelty, our approach combines formal verification and simulation-based testing for achieving a scalable analysis of the system's software. In addition, we explicitly separate the specification and verification of functional behavior and reconfiguration behavior for further improving the scalability of the verification. We evaluated all of our contributions based on the RailCab system and conducted two case studies that demonstrate the viability of our techniques.