Unvollständige Model Checking für Objektorientierte Nebenläufige Systeme
Beschreibung
Das Ziel des Projektes ist es, automatische Verifikationstechniken auf hierarchische objektorientierte Modelle (wie z.B. UML-RT) anwendbar zu machen. Da diese Modelle bei praktischen Anwendungen häufig sehr große oder unendliche Zustandsräume besitzen, versagen klassische automatische Model Checking Algorithmen bei ihrer Analyse. In dem Projekt sollen erstens verschiedene unvollständige 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.
Teilnehmer
Institutionen
- FB Informatik und Informationswissenschaft
Mittelgeber
Name | Kennziffer | Beschreibung | Laufzeit |
---|---|---|---|
Deutsche Forschungsgemeinschaft | 612/04 |
Weitere Informationen
Laufzeit: | 01.01.2004 – 30.08.2005 |