Sichere Integration von Lernen in Autonomen cyber-physischen Systemen (Safe ILIAS)

Grunddaten zu diesem Projekt

Beschreibung

Cyber-physische Systeme sind Systeme, die diskrete Kontrolle mit physischen Aspekten kombinieren. Beispiele dafür finden sich in Autos, Flugzeugen oder der Wasserversorgung. Mit dem aktuellen Trend zu selbstfahrenden Autos und smarten Infrastrukturen werden diese Systeme zunehmend autonom. Das bedeutet, dass sie lernen, gute Kontrollentscheidungen in unvorhergesehenen Situationen und dynamischen Umgebungen zu treffen. Das Lernen erhöht zwar ihre Flexibilität, aber auch ihre Komplexität. Gleichzeitig haben Fehler in cyber-physischen Systemen oft schwerwiegende Folgen, da sie zu großen finanziellen Verlusten oder sogar zum Verlust von Menschenleben führen können. Daher sind die Korrektheit und Zuverlässigkeit dieser Systeme von entscheidender Bedeutung. Formale Verifikationstechniken, die die Korrektheit mit Hilfe rigoroser mathematischer Methoden nachweisen, können uns Garantien für entscheidende Sicherheitseigenschaften von cyber-physischen Systemen geben. Allerdings ist formale Verifikation enorm teuer. Techniken zur automatischen Verifikation erkunden den zugrunde liegenden Zustandsraum eines gegebenen Systems, der oft zu groß ist, um vollständig erforscht zu werden. Deduktive Verifikationstechniken bieten einen mächtigen Lösungsansatz für dieses Problem, indem sie abstrakte mathematische Beweisführung nutzen, aber sie erfordern enormen Aufwand und Expertise, um die notwendigen Abstraktionen und Beweisideen für den Verifikationsprozess bereitzustellen. Dieses Problem ist bei autonomen cyber-physischen Systemen besonders schwerwiegend, da die beim Lernen üblicherweise verwendeten Versuch-und-Irrtum-Prozesse und statistischen Methoden nur schwer formal erfasst werden können. Das Ziel dieses Projekts ist die sichere Integration des Lernens in autonome cyber-physische Systeme mit vertretbarem Aufwand. Unser Schlüsselkonzept, um dies zu erreichen, ist Wiederverwendbarkeit. Insbesondere erforschen wir wiederverwendbare Abstraktionen für autonome cyber-physische Systeme. Durch die Bereitstellung neuartiger Konzepte zur systematischen Wiederverwendung von formalen Spezifikationen und Abstraktionen (z.B. Eigenschafts- und Spezifikationsmuster) werden wir den manuellen Aufwand und die erforderliche Expertise deutlich reduzieren und damit die Anwendbarkeit und Akzeptanz der deduktiven Verifikation in industriellen Entwurfsprozessen für autonome cyber-physische Systeme erhöhen.