SAPHIR – Ein Systematischer Ansatz zur Prüfung Hybrider Intelligenter systeme auf Resilienz

• Antragstellerinnen: Professorin Dr.-Ing. Paula Herber; Professorin Dr. Anne Remke
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 573591922

Cyber-physikalische Systeme (CPS) spielen eine zunehmend zentrale Rolle in der modernen Gesellschaft. Sie kommen in komplexen sicherheitskritischen Anwendungen zum Einsatz – von essenziellen Infrastrukturen wie Energie- und Wasserversorgung bis hin zu autonomen Systemen wie Robotern und selbstfahrenden Fahrzeugen. Die Gewährleistung von Sicherheit, Leistungsfähigkeit und Resilienz dieser Systeme stellt eine große Herausforderung dar, insbesondere aus drei Gründen: Erstens sind CPS hybride Systeme, die diskretes und kontinuierliches Verhalten kombinieren. Zweitens unterliegen CPS Unsicherheiten wie Sensorausfälle oder -rauschen. Drittens nutzen CPS zunehmend lernbasierte Verfahren zur intelligenten Steuerung in dynamischen Umgebungen. Kompositionale formale Methoden wie die deduktive Verifikation ermöglichen eine modulare Verifikation strikter Korrektheitsgarantien. Allerdings ignorieren diese Methoden jedoch häufig Unsicherheiten oder basieren auf übermäßig konservativen Annahmen. Quantitative modellbasierte Evaluierungstechniken wie das statistische Model Checking oder Erreichbarkeitsanalysen für stochastische Systeme bieten hingegen auch unter Unsicherheit statistische Garantien. Allerdings sind sie jedoch auf bestimmte Systemklassen und zeitlich begrenzte Eigenschaften beschränkt. Das Projekt SAPHIR – A Systematic Approach for Provably Correct Hybrid Systems that are Intelligent and Resilient zielt darauf ab, die Lücke zwischen diesen grundlegend unterschiedlichen Ansätzen zu schließen. Ziel ist die Entwicklung neuer Methoden, die eine kompositionale und quantitative Verifikation hybrider Systeme unter Unsicherheit ermöglichen. SAPHIR basiert auf drei Kernideen: (1) neuartige Modellierungstechniken, die Unsicherheiten formal erfassen und sowohl mit deduktiver Verifikation als auch mit quantitativen Evaluierungstechniken kompatibel sind, (2) neue Verfahren zur Zerlegung komplexer Anforderungen in kontextabhängige Service Level zur Unterstützung skalierbarer kompositionaler Analysen quantitativer Eigenschaften, und (3) Strategien zur sicheren Integration von lernbasierten Komponenten. Diese Forschung legt das methodische Fundament für intelligente und resiliente CPS, die nicht nur leistungsfähig, sondern auch nachweislich korrekt sind.

• DFG-Verfahren: Sachbeihilfen