Verifikationstechniken für Petrinetze auf Multicore-Architekturen

• Antragsteller: Professor Dr. Karsten Wolf
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2012 bis 2014
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 210313419

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.

• DFG-Verfahren: Sachbeihilfen