In this work, a new assertion language and verification framework has been developed. It enables the specification and validation of temporal properties accross different abstraction levels. This new language is required because existing assertion languages do only offer limited support for the verification of abstract, nonsynthesizable models. The semantics of the language is defined by a mapping onto a high-level colored petri net. The advantageous applicability of this language has been shown over several applications by using a compiler-based framework and a specific assertion kernel.     «

In this work, a new assertion language and verification framework has been developed. It enables the specification and validation of temporal properties accross different abstraction levels. This new language is required because existing assertion languages do only offer limited support for the verification of abstract, nonsynthesizable models. The semantics of the language is defined by a mapping onto a high-level colored petri net. The advantageous applicability of this language has...     »

Im Rahmen dieser Arbeit wurde eine neue Assertionsprache und Verifikationsumgebung entwickelt, welche die Spezifizierung und Validierung von temporalen Modelleigenschaften über Abstraktionsebenen hinweg ermöglicht. Die Entwicklung der Sprache ist notwendig weil existierende Assertionsprachen die Anwendung auf nicht synthetisierbare abstrakte Modelle nur eingeschränkt ermöglichen. Die formale Semantik der Sprache wurde durch die Abbildung auf ein abstraktes gefärbtes Petrinetz definiert. Die vorteilhafte Anwendbarkeit der Sprache wurde durch einen Compiler und einen speziellen Assertionkernel in mehreren Anwendungen nachgewiesen.     «

Im Rahmen dieser Arbeit wurde eine neue Assertionsprache und Verifikationsumgebung entwickelt, welche die Spezifizierung und Validierung von temporalen Modelleigenschaften über Abstraktionsebenen hinweg ermöglicht. Die Entwicklung der Sprache ist notwendig weil existierende Assertionsprachen die Anwendung auf nicht synthetisierbare abstrakte Modelle nur eingeschränkt ermöglichen. Die formale Semantik der Sprache wurde durch die Abbildung auf ein abstraktes gefärbtes Petrinetz defin...     »