Dynamische, Hybride und Probabilistische Systeme: Verifikation & Erklärung ((13) A12*)

Klassische Verifikationstechniken dienen dazu, zu prüfen ob ein System eine gegebene Eigenschaft hat oder nicht. Dies ist in der Praxis oft unzureichend, da solche Ergebnisse allein nicht verstehbar sind. Verifikationstechniken sollten stattdessen besser beleuchten, warum eine zu verifizierende Eigenschaft gilt oder nicht, und inwieweit Zustände, Systemkomponenten oder Parameter einen Einfluss auf die Erfüllung oder Verletzung einer Eigenschaft haben. Projekt A12 entwickelt das theoretische Fundament für verstehbare Verifikationstechniken für dynamische Systeme, hybride Automaten, sowie probabilistische Systeme. Dies umfasst verschiedene Konzepte von Robustheit, quantitative Zuschreibung von Verantwortung, und Ursache-Wirkung-Beziehungen in operationellen Modellen.

DFG-Verfahren Transregios

Teilprojekt zu TRR 248:  Grundlagen verständlicher Software-Systeme - für eine nachvollziehbare cyber-physische Welt

Antragstellende Institution Universität des Saarlandes

Teilprojektleiterinnen / Teilprojektleiter Professorin Dr. Christel Baier; Professor Dr. Rupak Majumdar; Professor Dr. Joël Ouaknine