GRK 2428:  CONVEY - Continuous Verification of CYber-Physical Systems

• Fachliche Zuordnung: Informatik
• Förderung: Förderung seit 2019
• Webseite: Zur Homepage
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 378803395

Zunehmend wurden In den letzten Jahren Netzwerke, Computer, Sensoren und Aktuatoren Teil cyber-physikalischer Systeme (CPS), d.h. Softwaresysteme, die mit dem kontinuierlichen Verhalten ihrer Umwelt umgehen müssen. CPS haben eine Komplexität erreicht, die viele Herausforderungen und Forschungsmöglichkeiten in den Bereichen Software Engineering, Kontrolltheorie und Informatik im Allgemeinen eröffnet. Zusätzlich haben Methoden der KI begonnen, eine immer stärkere Rolle in CPS zu spielen. Da CPS oft sicherheitskritisch sind, sollte ihr Entwurf und ihr Einsatz von einer umfassenden Überprüfung, wenn nicht gar Verifizierung ihres Verhaltens begleitet werden, die auf einer semantischen Grundlage beruhen. Die Integration von KI hat hat diese Aufgabe zusätzlich erschwert. In der ersten Förderperiode haben wir bereits einige Aspekte der Integration von KI, insbesondere maschinellem Lernen berücksichtigt. In der zweiten Förderperiode planen wir, diese Richtung zu verstärken und Techniken zu erforschen für Entwurf oder formale Verifizierung von KI-gestützten Systemen, die mit einer sich verändernden Umgebung interagieren. Veränderung ist eine grundlegende Herausforderung bei der Verifizierung von CPS unabhängig davon, ob sie KI-gestützt sind oder nicht: (1) Die Anforderungen ändern sich. Während in anderen Bereichen der Softwareentwicklung die meisten Änderungswünsche auf neues oder anderes funktionales Verhalten zielen, sehen sich die Entwickler von KI-gestützten CPS immer häufiger mit nicht funktionalen Änderungswünschen konfrontiert, z. B. für schnellere Reaktionszeiten und geringeren Stromverbrauch. (2) Das verfügbare Wissen ändert sich, oder die gesamte Implementierung. Während ersteres von der Erfassung weiterer Daten oder Lernen zurückzuführen ist, kann sich letzteres auch aufgrund von Refactoring oder neuer Hardware ergeben. (3) Die physische Umgebung ändert sich ständig und in einer Weise, die in der Entwurfsphase nicht absehbar ist. Idealerweise sollte sich das System selbständig an diese Veränderungen anpassen. Daraus ergibt sich eine Dimension der Veränderung, die sich qualitativ von den vorhergehenden unterscheidet. Künftige Technologien für den Entwurf und die Verifizierung KI-gestützter CPS müssen kontinuierliche Daten, kontinuierliches Verhalten, kontinuierliche Entwicklung, kontinuierliches Lernen sowie kontinuierliche Analyse und Synthese zusammen berücksichtigen. Die Verifikationstechniken für KI-gestützte Komponenten stecken allerdings noch in den Kinderschuhen. Der Umgang mit Veränderungen auf der Anforderungs-, Implementierungs- und Umgebungsebene für KI-gestützte CPS erfordert eine Verbindung von Kontrolltheorie, künstlicher Intelligenz und formalen Methoden. Nur dann wird es wird es möglich sein, KI-gestützte CPS zu realisieren für fortschrittliche medizinische Geräte, menschenfreundliche Roboter oder autonome Fahrzeuge, die im öffentlichen Raum operieren.

• DFG-Verfahren: Graduiertenkollegs
• Antragstellende Institution: Ludwig-Maximilians-Universität München
• Mitantragstellende Institution: Technische Universität München (TUM)
• Sprecher: Professor Dr. Dirk Beyer
• beteiligte Wissenschaftlerinnen / beteiligte Wissenschaftler: Professorin Dr. Susanne Albers; Professor Dr.-Ing. Matthias Althoff; Professor Dr. Jasmin Christian Blanchette; Professor Dr. Javier Esparza; Professor Debarghya Ghoshdastidar, Ph.D.; Professorin Dr. Marie-Christine Jakobs; Professor Dr. Johannes Kinder; Professor Jan Kretinsky, Ph.D.; Professorin Dr. Angela Schoellig; Professor Dr. Majid Zamani