A New Assertion Language Covering Multiple Levels of Abstraction
Volkan Esen · mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich) · 2008
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.