Modell-basierte Verifikation von vernetzten mechatronischen Systemen

Know about the book -

Modell-basierte Verifikation von vernetzten mechatronischen Systemen is written by Martin Hirsch and published by Logos Verlag Berlin GmbH. It's available with International Standard Book Number or ISBN identification 3832520783 (ISBN 10) and 9783832520786 (ISBN 13).

Beim Entwurf selbstoptimierender, mechatronischer Systeme stellt die eingebettete Software einen grossen Teil der Wertschopfung 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 uber die Aufnahme von System- und Umweltdaten durch Sensorik hinaus. Hier werden ggf. komplexe Zustandsinformationen uber entsprechende Protokolle und zugrunde liegende Kommunikationskanale ausgetauscht, die dann wieder das Verhalten bzw. die zugrunde liegenden Berechnungen der einzelnen Komponenten massiv beeinflussen konnen. Diese Entwicklung fuhrt zu ausserst komplexer hybrider (diskreter / kontinuierlicher) Software. Des Weiteren werden selbstoptimierende, mechatronische Systeme oftmals in sicherheitskritischen Umgebungen eingesetzt. Hierdurch mussen formale Verfahren zur Verifikation der Korrektheit des Systems gegenuber 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 unterstutzt einen kompositionellen Verifikationsansatz fur das Echtzeitverhalten von mechatronischen Systemen. Um eine effiziente Verifikation solcher vernetzten mechatronischen Systeme zu ermoglichen, werden in dieser Arbeit Techniken der Abstraktion, Dekomposition sowie der regelbasierten Modellierung eingefuhrt. Hierbei werden diese nicht orthogonalen Techniken geschickt miteinander kombiniert. Ziel ist es, die besonders durch die Verwendung domanenubergreifender Modelle, wie sie bei der Modellierung von mechatronischen Systemen vorkommen, entstehenden inharenten multi-Paradigmenwechsel modellieren zu konnen. 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.