Starten Sie Ihre Suche...


Durch die Nutzung unserer Webseite erklären Sie sich damit einverstanden, dass wir Cookies verwenden. Weitere Informationen

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

Laufzeit: 01.01.2004 - 31.12.2015

Partner: Andere Teilprojektleiter in diesem Projekt: - 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

Förderung durch: DFG TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme, Teilprojekt R1

Website

Kurzfassung


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...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.» weiterlesen» einklappen

Projektteam


Beteiligte Einrichtungen