Model Checking of Reconfigurable Petri Nets

Abstract

Ein wichtiges Ziel der theoretischen Informatik ist die Entwicklung formaler Methoden, die es erlauben die Qualität der zu entwickelnden Sofware zu verbessern. Eigenschaften wie Lebendigkeit, Verklemmungen und Sicherheiten k¨onnen f¨ur ein gegebenes Modell nachgewiesen werden. Hierfür eignet sich das Modellieren mit Petri-Netzen als eine etablierte wissenschfftliche Technik besonders gut. Basierend auf Petri-Netzen, erweitern rekon gurierbare Petri-Netze die Netze um eine Menge von Regeln, die genutzt werden um das Netz dynamisch zu verändern. Bisher fehlt die Möglichkeit der Verifizierung von rekonfigurierbaren Petri-Netzen. Diese Thesis beschreibt die Überführung von rekonfigurierbaren Petri-Netzen zu einem Maude Netz. Ziel dieser Master Thesis ist der Nachweis der Korrektheit des Maude Netzes.

One important aim of theoretical computer science is model checking to improve the software quality. Propert es such as liveness, deadlock or safety can be veri ed for a given model. Modelling with Petri nets is a typical technique because it is well understood and can be used for model checking. Recon gurable Petri nets are extending the concept of Petri nets with a set of rules that can be used dynamically to change the net. e possibility to verify a recon gurable Petri net and properties such as deadlocks or liveness is non-existent. e aim of this thesis is the proof of correctness of a Maude net.