Erreichbarkeitsanalyse für stochastische hybride Systeme

• Antragstellerinnen: Professorin Dr. Anne Remke; Professorin Dr. Erika Ábrahám
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 471367371

Unsere Gesellschaft und Wirtschaft hängen von der Zuverlässigkeit von sehr komplexen und dynamischen sicherheitskritischen Systemen ab. Die Nutzer dieser Systeme müssen sich auf deren Funktionalität verlassen können. Unbekannte Faktoren in der Umgebung, Sicherheitslücken und Fehler in Geräten stellen eine ernsthafte Gefahr für ihre zuverlässige Arbeitsweise dar.Das Ziel formaler Methoden ist es, Modellierungsansätze und Analysemethoden zu schaffen, die die Zuverlässigkeit einzelner Systeme verbessern. Stochastische hybride Modelle eignen sich gut, um eine Bandbreite an relevanten Systemen zu modellieren, bei denen diskrete, kontinuierliche und stochastische Aspekte eine Rolle spielen. Durch die Ausdrucksstärke dieser Modelle wird ihre Analyse zu einer Herausforderung, für die aktuell nur wenige Software-Werkzeuge vorhanden sind. Diese Ansätze nutzen Abstraktion und Approximation, wobei die Präzision mit wachsender Modellgröße abnimmt.Unser Ziel ist es, bessere Algorithmen und Werkzeuge für die Erreichbarkeitsanalyse stochastischer hybrider Modelle zu schaffen, welche auf der separaten Analyse hybrider und stochastischer Aspekte basieren. Dieses Vorgehen war in der Vergangenheit schon erfolgreich für stochastische Petri-Netze, welche im Allgemeinen nebenläufiges Verhalten gut abbilden können und inhärent kompositional sind.In diesem Projekt wird die Expertise der Projektpartner auf den Gebieten Erreichbarkeitsanalyse hybrider Systeme, probabilistischer Systeme und stochastischer Erweiterungen hybrider Petri-Netze kombiniert, um Synergieeffekte zu schaffen: Unser Ziel ist es, zunächst eine kompositionelle Erreichbarkeitsanalyse für hybrides Verhalten zu entwickeln, um in einem zweiten Schritt das stochastische Verhalten über multi-dimensionale Integration einfließen zu lassen. Wir erwarten, dass dieser Ansatz die Effizienz und Anwendbarkeit einer größeren Modellklasse ermöglicht.Wir werden Analysemethoden für automatenbasierte stochastische hybride Modelle entwickeln und über eine Transformation ihre Anwendbarkeit für Petri-Netz Modelle sicherstellen.Für (rein) hybride Automaten wurden in der Vergangenheit bereits effiziente Analysemethoden entwickelt. Wir werden untersuchen, wie diese Ansätze für stochastische hybride Modelle genutzt werden können. Mit dem Ziel, die Skalierbarkeit zu erhöhen, werden wir die Kompositionalität unserer Modelle in der Analyse ausnutzen, daher werden Teile unseres Projektes einen doppelten Nutzen haben, da sie auch die Analyse nicht-stochastischer hybrider Systeme verbessern.Neben den theoretischen Entwicklungen werden wir unsere Methoden implementieren, gründlich evaluieren und als Softwaretool für Endnutzer bereitstellen. Da alle Entwicklungen öffentlich verfügbar sein werden, können sie in der Zukunft für die schnelle prototypische Entwicklung weiterer Verifikationsmethoden genutzt werden. Unsere Entwicklungen werden mit Hilfe von typischen Fallstudien für sicherheitskritische Systeme validiert.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Österreich
• Kooperationspartner: Dr. Stefan Schupp