Das Gesamtziel des Projekts ist die Entwicklung eines interoperablen Kalküls für die interaktive Verifikation komplexen, nebenläufiger Systeme. Die Interoperabilität bezieht sich auf 4 Aspekte: Das Zusammenspiel verschiedener Temporallogiken untereinander (Z1), die Integration verschiedener Besehreibungsformalismen für dynamische Systeme in die Logik (Z2), das Umschalten zwischen temporallogischer und algebraischer Verifikation (Z3) und die Verzahnung von Verifikation, Modifikation und Wiederverwendung von Beweisen (Z4). Ein solcher Kalkül ist für die interaktive Verifikation komplexen verteilter Anwendungen erforderlich, die vielschichtig sind, sehr große oder unendliche Zustandsräumen haben, und die sich nicht mit einer einzigen Modellierungs- oder Verifikationstechnik (oder gar vollautomatisch) behandeln lassen. In der ersten Projektphase wurden die grundlegenden Konzepte sowie ein Kalkül entwickelt, der im Sinne eines 'vertikalen Prototyps' die Tragfähigkeit des Ansatzes für ein Teilspektrum der Logiken illustriert. Diese Arbeiten sollen in der nächsten Phase entsprechend erweitert und fortgesetzt werden. Als neue Ziele kommen die 'Graphische Beweisführung' sowie die Durchführung vergleichender Fallstudien hinzu.
DFG Programme
Research Grants
