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

The subproject aims at a significant improvement of the automatic verification of rich specifications of systems containing the three aspects control flow, data types and real-time requirements. As a concrete expression of a specification formalism, the language CSP-OZ-DC will be used, which combines CSP (Communicating Sequential Processes), Object-Z (OZ) and Duration Calculus (DC). The verification of real time properties of such specifications shall be achieved by a combination of compositional methods with symbolic algorithms.