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