Modellierung und Verifikation von sicheren und performanten cyberphysikalischen Systemen

• Antragsteller: Professor Dr. Christoph Grimm; Professor Dr. Klaus Schneider
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 530118585

Cyber-physikalische Systeme (CPS) werden zu einem immer wichtigeren Bestandteil kritischer Infrastrukturen. CPS finden sich in autonomen Fahrzeugen, Flugzeugen, medizinischen Geräten, intelligenten Stromnetzen und intelligenten Fabriken. Neben funktionalen Anforderungen müssen CPS auch nicht-funktionale Anforderungen wie Echtzeitverhalten bei begrenztem Energieverbrauch erfüllen. Aufgrund sicherheitskritischer Anwendungen ist eine Verifikation oft zwingend erforderlich, um Fehlverhalten mit katastrophalen Folgen zu vermeiden. CPS sind von Natur aus offen, da sie mit anderen Systemen zusammenarbeiten müssen. Darüber hinaus müssen CPS auch nach dem ersten Einsatz (häufig) aktualisiert werden, da spätere Aktualisierungen ihrer Umgebung dies erforderlich machen. Die vernetzte Implementierung von CPS bringt weitere Schwierigkeiten mit sich, so dass die Cybersicherheit noch schwieriger zu handhaben ist, da die Kommunikation zwischen vernetzten Systemen prinzipiell angegriffen werden kann. Modellbasierte Entwurfsmethoden haben sich sowohl für den Entwurf eingebetteter Systeme als auch für den Entwurf cyber-physikalischer Systeme bewährt. Ein solcher Entwurf beginnt mit einem hardwareunabhängigen Modell des Systems, das hinsichtlich funktionaler Anforderungen verifiziert werden kann. Nicht-funktionale Anforderungen wie Performanz, Energieverbrauch und Sicherheit können auf dieser Ebene jedoch noch nicht behandelt werden, da diese Eigenschaften von der HW/SW-Partitionierung und den vernetzten Komponenten abhängen. Dennoch ist dieser erste modellbasierte Entwurf sehr nützlich, um auch die nicht-funktionalen Anforderungen zu erfüllen, da aus dem Modell verschiedene korrekte Systemimplementierungen in einer Entwurfsraumexploration abgeleitet werden können. Statische Analyse und virtuelle Prototypen gehören zu den Techniken, auf die wir uns in dieser Optimierungsphase stützen werden. Die Korrektheit der Systeme ist unser primäres Ziel. Allerdings kann die spätere Implementierung neuer Sicherheitsmechanismen in aktualisierten Versionen eines CPS dessen Reaktionszeit und Echtzeitverhalten beeinträchtigen. Wir schlagen daher vor, die Korrektheits-, Sicherheits- und Leistungsanforderungen (und ihre wechselseitigen Beziehungen) während des gesamten Lebenszyklus des CPS zu erhalten, indem digitale Zwillinge verwendet werden, die diese Anforderungen erfüllen können und explizite Sicherheitsmechanismen enthalten. Die Sicherheits- und Leistungsanforderungen dieses Entwurfs werden damit validiert. Das System wird dann mit automatisierten Überwachungstechniken implementiert, die auf Laufzeitmonitoren basieren, um Sicherheits- oder Leistungsprobleme zur Laufzeit zu erkennen. Erkannte Probleme werden dann in die Entwurfsmodelle zurückgeführt, die dann aktualisiert werden, z.B. mit neuen Sicherheitsmechanismen. Die Ergebnisse werden anhand eines Smart-Grid-Management Systems aus einem früheren EU-Projekt evaluiert und demonstriert.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Frankreich
• Kooperationspartnerinnen / Kooperationspartner: Professor Dr. Ludovic Apvrille; Professorin Dr. Daniela Genius; Professorin Dr. Ahlem Mifdaoui