Verifikationstechniken für Petrinetze auf Multicore-Architekturen
Final Report Abstract
Für die Mehrzahl der untersuchten Techniken konnten (unterschiedlich große) Laufzeitgewinne dadurch erzielt werden, dass Multicore-Architekturen gezielt ausgenutzt wurden. Dadurch können, in produktiver Konkurrenz zu symbolischen Modelchecking-Verfahren, die expliziten und strukturellen Techniken für Petrinetze als sinnvolle und leistungsstarke Alternative bei der Verifikation verteilter Systeme aufrechterhalten werden. Dies ist in Wettwerebssituationen wie dem Model Checking Contest nachweisbar. Über die konkreten Arbeitspakete hinaus zeigt sich, dass die Laufzeitverbesserung mit der Größe der jeweils parallel bearbeiteten Teilprobleme korreliert. Das ist einerseits nicht überraschend, durch das Projekt kann aber die sinnvolle Mindestgröße besser abgeschätzt werden. Dies nutzen wir zur weiteren Verbesserung unserer Werkzeuge in wissenschaflich weniger interessanten Bereichen wie z.B. der Verwaltung und Vorverarbeitung der zu verifizierenden Petrinetze. Hier sind bereits Bachelor- und Masterarbeiten angesetzt. Die leistungsstärkeren Werkzeuge gestatten die erfolgreiche Lösung einer größeren Zahl von Problemen in verschiedenen Anwendungsfeldern. Für LoLA sind das unter anderem: die Exploration biochemischer Reaktionsketten mithilfe des Pathway Logic Assistant vom SRI; die Komposition von Webservices (in Zusammenarbeit mit der Gruppe von Prof. Penczek); die Verifikation asynchroner Schaltkreise, wo einige bislang nicht beherrschte Instanzen als deadlockfrei nachgewiesen werden konnten.
