>

DFG Projekt:
Unvollständiges Model Checking für Objektorientierte Systeme

Das Ziel des Projektes ist es, automatische Verifikationstechniken auf hierarchische objektorientierte Modelle (wie z.B. UML-RT) anwendbar zu machen. Erstens sollen verschiedene Model Checking Algorithmen und andere Techniken (z.B. Akzeleration) auf ihre Anwendbarkeit auf UML-RT Modelle untersucht werden. Zweitens soll eine zentrale Schnittstelle geschaffen werden, die ein gegebenes Modell analysiert, die geeignetste Verifikationsmethode auswählt und die Ergebnisse interpretiert und für den Benutzer darstellt.