Modell-basierte Verifikation von vernetzten mechatronischen Systemen

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.