Model Checking Object Petri Nets in Maude and Prolog

;

URN urn:nbn:de:gbv:18-228-7-608
URL
Dokumentart: Report (Bericht)
Schriftenreihe: Berichte des Fachbereichs Informatik der Universität Hamburg
Bandnummer: 258
Sprache: Englisch
Erstellungsjahr: 2004
Publikationsdatum:
SWD-Schlagwörter: Kompilation , Model Checking , Animation , PROLOG <Programmiersprache>
Freie Schlagwörter (Deutsch): Objekt-Petrinetze
Freie Schlagwörter (Englisch): Object Petri Nets , Model Checking , Prolog , Animation , Compilation
DDC-Sachgruppe: Informatik
BK - Klassifikation: 54.10

Kurzfassung auf Englisch:

Object Petri nets (OPNs) provide a natural and modular method for modelling many realworld systems. We give a structure-preserving translation of OPNs to Prolog by encoding the OPN semantics, avoiding the need for an unfolding to a flat Petri net. The translation provides support for reference and value semantics, and even allows different objects to be treated as copyable or non-copyable. The method is developed for OPNs with arbitrary nesting. We then apply logic programming tools to animate (i.e. execute), compile and model check OPNs. In particular, we use the partial evaluation system logen to produce an OPN compiler, and we use the model checker xtl to verify CTL formulae. We also use logen to produce special purpose model checkers. We present two case studies, along with experimental results. A comparison of OPN translations to Maude specifications and model checking is given, showing that our approach is roughly twice as fast for larger systems. We also tackle infinite state model checking using the ecce system.

Kurzfassung auf Deutsch:

Objekt-Perinetze (OPN) stellen ein nat¨urliches und modulares Mittel zur Modellierung vieler Systeme dar. In diesem Bericht beschreiben wir eine Struktur erhaltende Übersetzung von Objekt-Petrinetzen nach Prolog, die auf einer Kodierung der OPN-Semantik basiert und somit das Entfalten des OPN zu einem einfachen Petrinetz überflüssig macht. Die Übersetzung unterstützt sowohl Referenz- als auch Wertsemantiken. Kombinationen dieser Semantiken innerhalb eines Netztes sind in diesem Formalismus ebenso m¨oglich und die Übersetzung erlaubt beliebige Schachtelungstiefen der Objektnetze. Es werden bekannte Werkzeuge aus dem Bereich der Logikprogrammierung eingesetzt, um Objekt-Petrinetze zu animieren (d.h. auszuführen), zu kompilieren und zu verifizieren (durch Model-Checking). Dabei wird von logen Gebrauch gemacht, um ein kompiliertes Netz zu erhalten, auf dem der CTL-Model-Checker xtl effizient arbeiten kann. logen wird zudem eingesetzt, um noch effizientere Model-Checker für spezielle Netze zu generieren. Es werden zwei Fallbeispiele untersucht und hierf¨ur werden experimentelle Ergebnisse präsentiert. Eine kurze Gegenüberstellung mit einer bekannten OPN- Übersetzung in Maude zeigt, dass in der Übersetzung nach Prolog für größere Systeme das Model-Checking etwa doppelt so schnell ist.

Hinweis zum Urherberrecht

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.