Über Realzeitautomaten hinaus (R01)

• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2004 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999

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.

• DFG-Verfahren: Transregios
• Teilprojekt zu: TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme
• Antragstellende Institution: Carl von Ossietzky Universität Oldenburg
• Mitantragstellende Institution: Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik; Universität des Saarlandes
• Teilprojektleiterinnen / Teilprojektleiter: Professor Dr. Bernd Finkbeiner; Professor Dr. Martin Fränzle; Professor Dr. Ernst-Rüdiger Olderog; Professor Dr. Andreas Podelski; Professorin Dr. Viorica Sofronie-Stokkermans