Bibliographie

Model Checking Object Petri Nets in Maude and Prolog

Berndt Farwer and M. Leuschel.
Model checking object Petri nets in Maude and Prolog.
Technical Report FBI-HH-B-258/04, Fachbereich Informatik, Universität Hamburg, 2004.

Kurzfassung: Bisher nicht verfügbar.

BibTeX-Eintrag

@techreport{Farwer+04,
    Abstract = {Object Petri nets (OPNs) provide a natural and modular
method for the modelling of many real-world systems. We give a
structure-preserving translation of OPNs to Prolog, 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, respectively. The method is
developed for OPNs with arbitrary nesting. We then apply logic
programming tools to animate, 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 formulas.
We also use LOGEN to produce special purpose model checkers. We present
two case studies, along with experimental results. A comparison to 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.},
    Author = {Farwer, Berndt and Leuschel, M.},
    Institution = {Fachbereich Informatik, Universit{\"a}t Hamburg},
    Number = {FBI-HH-B-258/04},
    Title = {Model Checking Object {Petri} Nets in {Maude} and {Prolog}},
    Year = 2004
}

Copyright-Hinweis

Diese Informationen werden zur Verfügung gestellt, um technische und Forschungsarbeiten zeitnah bekannt zu geben. Das Urheberrecht und alle damit verbundenen Rechte verbleiben bei den Autoren bzw. anderen Rechteinhabern. Von jedem, der Informationen dieser Seiten übernimmt, wird erwartet, dass er sich an die jeweiligen Bedingungen und Beschränkungen der Rechteinhaber hält. Meist bedeutet dies, dass die hier bereitgestellten Daten nicht ohne explizite Genehmigung der Rechteinhaber weiterveröffentlicht werden dürfen.