Unvollständige automatische Verifikation von Software-Designmodellen für nebenläufige objektorientierte eingebettete Echtzeitsysteme basierend auf dem Paradigma der erweiterten kommunizierenden Zustandsautomaten.

• Antragsteller: Professor Dr. Stefan Leue
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2002 bis 2010
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5364050

Das Ziel des Projekts 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 diesem 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 Ergenisse interpretiert und für den Benutzer darstellt.

• DFG-Verfahren: Sachbeihilfen