English

Software has become the driving force in the development of self-optimzing mechatronic systems. Such systems include hard-realtime coordination, which is realized by software, at the network level between distributed componentes as well as controllers which are more and more implemented by software. The communication goes beyond the use of system and environmental data from controlers. If necessary, complex status information about appropirate protocols and communication channels are exchanged, which themself can massively influence the underlying behavior of the individual components. This development leads to extremely complex hybrid (discrete / continuous) software. In addition, self-optimizing mechatronic systems are often used in safety-critical environments. This enforces the use of formal verification techniques to ensure the correctness of specified properties.

In the context of this thesis new concepts and methods for the modelling and verification of these mechatronic systems are introduced and formally described. The new approach is based on the Mechatronic UML approch, developed in the Collaborative Research Center 614, which already supports a compositional verification approach for the pure real-time behavior of mechatronic systems.

In order to enable an efficient verification for such mechatrinic systems, techniques like abstraction, decomposition as well as rule-based modelling are introduced. Here, these non orthogonal techniques are skillfully combined. One aim is to handle all models specified by all different domains. The new approach for the model-based verification of mechatronic systems is massively characterized by the integration of efficient verification techniques for the different domains, based on their domain specific model-based knowledge.

Deutsch

Beim Entwurf selbstoptimierender, mechatronischer Systeme stellt die eingebettete Software einen großen Teil der Wertschöpfung dar. Typischerweise werden Regelungen oder Steuerungen in Software umgesetzt. Durch die starke Vernetzung selbstoptimierender Systeme wird Software auch zur nachrichtenbasierten Kommunikation und Koordination zwischen den einzelnen verteilten selbstoptimierenden Systemen eingesetzt. Diese Kommunikation geht über die Aufnahme von System- und Umweltdaten durch Sensorik hinaus. Hier werden ggf. komplexe Zustandsinformationen über entsprechende Protokolle und zugrunde liegende Kommunikationskanäle ausgetauscht, die dann wieder das Verhalten bzw. die zugrunde liegenden Berechnungen der einzelnen Komponenten massiv beeinflussen können. Diese Entwicklung führt zu äußerst komplexer hybrider (diskreter / kontinuierlicher) Software. Des Weiteren werden selbstoptimierende, mechatronische Systeme oftmals in sicherheitskritischen Umgebungen eingesetzt. Hierdurch müssen formale Verfahren zur Verifikation der Korrektheit des Systems gegenüber sicherheitskritischen Eigenschaften eingesetzt werden.

Im Rahmen dieser Dissertation werden nun Konzepte und Methoden zur Modellierung und Verifikation mechatronischer Systeme entwickelt und formal beschrieben. Der hier vorgestellte Ansatz baut auf dem im Sonderforschungsbereichs 614 entwickelten MechatronicUML Ansatz auf. Dieser unterstützt einen kompositionellen Verifikationsansatz für das Echtzeitverhalten von mechatronischen Systemen.

Um eine effiziente Verifikation solcher vernetzten mechatronischen Systeme zu ermöglichen, werden in dieser Arbeit Techniken der Abstraktion, Dekomposition sowie der regelbasierten Modellierung eingeführt. Hierbei werden diese nicht orthogonalen Techniken geschickt miteinander kombiniert. Ziel ist es, die besonders durch die Verwendung domänenübergreifender Modelle, wie sie bei der Modellierung von mechatronischen Systemen vorkommen, entstehenden inhärenten multi-Paradigmenwechsel modellieren zu können. Der hier vorgeschlagene Ansatz zur modell-basierten Verifikation mechatronischer Systeme zeichnet sich durch die Integration effizienter Verifikationstechniken, basierend auf dem Modellwissen und einer geschickten Modellierung, aus.