Automatische Verifikation von Qualitätsmerkmalen verteilter Systeme

• Applicant: Professor Dr.-Ing. Ulrich Herzog
• Subject Area: Theoretical Computer Science
• Term: from 1999 to 2002
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• Participating Person: Professor Dr. Joost-Pieter Katoen