Detailseite
Projekt
Theoretische Grundlagen und Model-Checking für Abstract-State-Machines
Antragsteller
Professor Dr. Erich Grädel
Fachliche Zuordnung
Theoretische Informatik
Förderung
Förderung von 1999 bis 2002
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5162256
Ziel dieses Vorhabens ist einerseits eine grundlegende Untersuchung ob, und wie effizient Model-Checking für Abstract-State-Machines durchgeführt werden kann, und andererseits die Bereitstellung komplexitäts- und modelltheoretische Grundlagen für Abstract-State-Machines.
Der Bereich der computergestützten Verifikation von ASM ist generell noch wenig erforscht. Angesichts der Erfolge der ASM-Verifikationsmethode bei der manuellen Verifikation ist eine prinzipielle Abschätzung der (Semi-) Automatisierbarkeit sinnvoll und dringend notwendig. Entgegen der beim Model-Checking üblichen Annahme, daß eine explizite Beschreibung des zu verifizierenden Systems bereits in Form einer Kripke-Struktur vorliegt, besteht die eigentliche Kernaufgabe beim Model-Checking von ASM genau in der Erzeugung und geeigneten (symbolischen) Beschreibung einer solchen Kripke-Struktur. Es sollen Klassen von ASM identifiziert werden, die eine (semi-) automatische Generierung der Kripke-Strukturen zulassen. Eine Erörterung der Komplexität dieser Generierung soll Kriterien für ASM liefern bei denen Model-Checking praktikabel ist.
Für die Verfeinerung und Weiterentwicklung der ASM-Methodik besteht inzwischen ein starker Bedarf an einer soliden theoretischen Fundierung von ASM. Im Bereich Theorie für ASM sind geplant: 1. eine komplexitätstheoretische Einordnung der wesentlichen algorithmischen ASM-Probleme (soweit diese entscheidbar sind). 2. die systematische Entwicklung einer Komplexitätstheorie für ASM, 3. die Erforschung des Zusammenhangs von ASM-Komplexität und Definierbarkeit in geeigneten logischen Systemen, 4. die Bereitstellung modelltheoretischer Grundlagen für ASM, insbesondere einer Kompositionstheorie.
Der Bereich der computergestützten Verifikation von ASM ist generell noch wenig erforscht. Angesichts der Erfolge der ASM-Verifikationsmethode bei der manuellen Verifikation ist eine prinzipielle Abschätzung der (Semi-) Automatisierbarkeit sinnvoll und dringend notwendig. Entgegen der beim Model-Checking üblichen Annahme, daß eine explizite Beschreibung des zu verifizierenden Systems bereits in Form einer Kripke-Struktur vorliegt, besteht die eigentliche Kernaufgabe beim Model-Checking von ASM genau in der Erzeugung und geeigneten (symbolischen) Beschreibung einer solchen Kripke-Struktur. Es sollen Klassen von ASM identifiziert werden, die eine (semi-) automatische Generierung der Kripke-Strukturen zulassen. Eine Erörterung der Komplexität dieser Generierung soll Kriterien für ASM liefern bei denen Model-Checking praktikabel ist.
Für die Verfeinerung und Weiterentwicklung der ASM-Methodik besteht inzwischen ein starker Bedarf an einer soliden theoretischen Fundierung von ASM. Im Bereich Theorie für ASM sind geplant: 1. eine komplexitätstheoretische Einordnung der wesentlichen algorithmischen ASM-Probleme (soweit diese entscheidbar sind). 2. die systematische Entwicklung einer Komplexitätstheorie für ASM, 3. die Erforschung des Zusammenhangs von ASM-Komplexität und Definierbarkeit in geeigneten logischen Systemen, 4. die Bereitstellung modelltheoretischer Grundlagen für ASM, insbesondere einer Kompositionstheorie.
DFG-Verfahren
Sachbeihilfen
