Number of cases campus Koblenz: 1 (warning level Gelb until 02.12.2020) Action plan

Über Realzeitautomaten hinaus (Teilprojekt TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme)

(AVACS-R1)

Period: Jan 01, 2004 - Dec 31, 2015
Status: abgeschlossen

Das Teilprojekt zielt auf eine deutliche Verbesserung der automatischen Verifikation von reichen Spezifikationenvon Systemen, die die drei Aspekte Kontrollfluss, Datentypen und Realzeitanforderungenbeinhalten. Als konkrete Ausprägung eines Spezifikationsformalismus soll die Sprache CSP-OZ-DCbenutzt werden, die CSP (Communicating Sequential Processes), Objekt-Z (OZ) und Duration Calculus(DC) kombiniert. Die Verifikation von Realzeiteigenschaften solcher Spezifikationen soll durcheine Kombination von kompositionellen Verfahren mit symbolischen Algorithmen erreicht werden.


Project partner

Prof. Dr. Bernd Finkbeiner,Universität des Saarlandes
Prof. Dr. Martin Fränzle, Carl von Ossietzky Universität Oldenburg
Prof. Dr. Ernst-Rüdiger Olderog, Carl von Ossietzky Universität Oldenburg

Prof. Dr. Andreas Podelski, Albert-Ludwigs-Universität Freiburg
Prof. Dr. Viorica Sofronie-Stokkermans, Max-Planck-Institut für Informatik und Universität Koblenz-Landau