Automatische Verifikation von Qualitätsmerkmalen verteilter Systeme

点击翻译按钮获取中文摘要

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.