Verifikationstechniken für Petrinetze auf Multicore-Architekturen

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

Seit einiger Zeit werden zur Steigerung der Leistungsfähigkeit von Hardwarearchitekturen verstärkt Multicore-Prozessoren eingesetzt. Dabei stellt sich heraus, dass eine optimale Nutzung der dadurch zur Verfügung stehenden Leistung nicht allein durch Compilertechniken erzielt werden kann. Statt dessen ist es sinnvoll, die Anwendungen selbst zu verteilen und dabei Einsichten über die implementierten Algorithmen zu nutzen. Eine besonders ressourcenintensive Klasse von Anwendungen sind Verfahren der computergestützten Verifikation. Zwar ist hier normalerweise der Speicherplatz die begrenzende Ressource, eine deutliche Verbesserung im Laufzeitverhalten könnte jedoch neue Anwendungen erschließen, z.B. eine stärkere Verzahnung von Modellierungs- und Verifikationstätigkeiten. Ziel dieses Vorhabens ist es, Verifikationstechniken für Petrinetze auf ihre sinnvolle Verteilbarkeit in Multicore-Architekturen zu untersuchen. Dabei werden sowohl zustandsraumbasierte Verfahren als auch strukturelle Analysetechniken betrachtet. In der Zustandsraumverifikation, wo es bereits einschlägige Arbeiten zur Organisation der eigentlichen Zustandsraumexploration gibt, liegt dabei der Schwerpunkt auf petrinetzspezifischen Aspekten von Zustandsraumreduktionstechniken.