Model Checking of Reconfigurable Petri Nets

URL
Dokumentart: Masterarbeit
Institut: Department Informatik
Sprache: Deutsch
Erstellungsjahr: 2015
Publikationsdatum:
SWD-Schlagwörter: Petri-Netz
DDC-Sachgruppe: Informatik

Kurzfassung auf Deutsch:

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.

Kurzfassung auf Englisch:

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.

Hinweis zum Urheberrecht

Für Dokumente, die in elektronischer Form über Datenenetze angeboten werden, gilt uneingeschränkt das Urheberrechtsgesetz (UrhG). Insbesondere gilt:

Einzelne Vervielfältigungen, z.B. Kopien und Ausdrucke, dürfen nur zum privaten und sonstigen eigenen Gebrauch angefertigt werden (Paragraph 53 Urheberrecht). Die Herstellung und Verbreitung von weiteren Reproduktionen ist nur mit ausdrücklicher Genehmigung des Urhebers gestattet.

Der Benutzer ist für die Einhaltung der Rechtsvorschriften selbst verantwortlich und kann bei Mißbrauch haftbar gemacht werden.