Automatische Verifikation von Qualitätsmerkmalen verteilter Systeme

• Antragsteller: Professor Dr.-Ing. Ulrich Herzog
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 1999 bis 2002
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5176626

Unser Ziel ist es, eine durchgängig verhaltensorientierte Methodik zu entwickeln, die die Spezifikation des Systems und des Leistungsmaßes auf demselben hohen Abstraktionsniveau erlaubt. Dazu soll eine verhaltensorientierte temporale Logik zur Spezifikation des Leistungsmaßes definiert werden. Weiterhin sollen Verfahren entwickelt werden, die die vollautomatische quantitative Verifikation der temporal-logischen Formeln ermöglichen. Beim Entwurf dieser sog. Model Checking-Algorithmen steht die Effizienz im Vordergrund. Dazu wollen wir die Reduktion des Zustandsraums sowie dessen kompakte Darstellung im stochastischen Kontext untersuchen.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Joost-Pieter Katoen