Beyond Timed Automata (R01)

• Subject Area: Software Engineering and Programming Languages
• Term: from 2004 to 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: CRC/Transregios
• Subproject of: TRR 14: Automatic Verification and Analysis of Complex Systems
• Applicant Institution: Carl von Ossietzky Universität Oldenburg
• Co-Applicant Institution: Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik; Universität des Saarlandes
• Project Heads: Professor Dr. Bernd Finkbeiner; Professor Dr. Martin Fränzle; Professor Dr. Ernst-Rüdiger Olderog; Professor Dr. Andreas Podelski; Professorin Dr. Viorica Sofronie-Stokkermans