Kurzfassung

Ziel der Arbeiten ist die (Weiter-)Entwicklung von Analysetechniken für Petri-Netze. Im Rahmen des Projekts ist ein Model-Checker entworfen und implementiert worden, der testet, ob ein Petri-Netz eine Spezifikation, ausgedrückt durch eine temporale-logische Formel, erfüllt. Als Datenstruktur für den Model-Checker ist eine Weiterentwicklung binärer Entscheidungsdiagramme erarbeitet worden, welche insbesondere bei der Analyse entfalteter höherer Petri-Netze bessere Ergebnisse als einfache...Ziel der Arbeiten ist die (Weiter-)Entwicklung von Analysetechniken für Petri-Netze. Im Rahmen des Projekts ist ein Model-Checker entworfen und implementiert worden, der testet, ob ein Petri-Netz eine Spezifikation, ausgedrückt durch eine temporale-logische Formel, erfüllt. Als Datenstruktur für den Model-Checker ist eine Weiterentwicklung binärer Entscheidungsdiagramme erarbeitet worden, welche insbesondere bei der Analyse entfalteter höherer Petri-Netze bessere Ergebnisse als einfache binäre Entscheidungsdiagramme liefert. Die aktuellen Arbeiten bestehen darin, den Model-Checker anhand von Beispielen aus der parallelen Programmierung auf seine Praxistauglichkeit zu testen. Weitere Informationen: e-mail: ridder@informatik.uni-koblenz.de.» weiterlesen» einklappen