Präzise Überwachung cyber-physischer Technologie unter Unsicherheit

• Antragsteller: Professor Dr. Bernd Finkbeiner; Professor Dr. Martin Fränzle
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Theoretische Informatik
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 521273327

Cyber-Physische Systeme (CPS), welche die physische Umgebung und zahlreiche eingebettete Computersysteme mittels digitaler Netzwerke zu einem eng gekoppelten Gesamtsystem verknüpfen, bilden die Schlüsseltechnologie der immer zahlreicher werdenden smarten Umgebungen. Die meisten dieser Anwendungen sind hochgradig sicherheitskritisch, da Fehlfunktionen der cyber-physischen Systeme unmittelbare Gefährdungen für Leib, Leben, Umwelt oder Güter nach sich ziehen. Die durchgängige Laufzeitüberwachung der Systemfunktionen durch geeignete Monitorprozesse stellt ein wichtiges Element zur Sicherstellung zuverlässigen, vorhersagbaren und sicheren Systemverhaltens dar. Die Anforderungen an die ein CPS überwachenden Monitorprozesse sind dabei extrem hoch, da fehlende Detektion von Ausnahmesituationen die vorgenannten Gefährdungen induziert, überflüssige Signalisierung umgekehrt die Systemleistung massiv herabsetzen kann. Das Projekt PreCePT leistet mittels eines Brückenschlags zwischen formalen Methoden der Informatik und Fehlermodellen der Messtechnik entscheidende Grundlagenforschung zur Deckung des Bedarfs an entsprechend zuverlässigen, nachweislich korrekten Monitorprozessen, indem es aus formalen Spezifikationen automatisch Laufzeitmonitore synthetisiert, welche die bei sensorischer Überwachung der Umwelt unvermeidbaren messtechnischen Ungenauigkeiten und partielle Beobachtbarkeit berücksichtigen. Die generierten Monitoringalgorithmen vereinen maximale Exaktheit mit harten Echtzeitgarantien und sind aufgrund stringenter Ableitung aus formalen semantischen Modellen von CPS sowie Nutzung fortschrittlicher arithmetischer Constraintsolvingtechniken in dieser Hinsicht nachweislich optimal.

• DFG-Verfahren: Sachbeihilfen