On-the-Fly Verification with PROD

Reference:

Kimmo Varpaaniemi. On-the-fly verification with PROD. In Jörg Desel, Andreas Oberweis, and Wolfgang Reisig, editors, Algorithmen und Werkzeuge für Petrinetze: Workshop der GI-Fachgruppe 0.0.1, ``Petrinetze und verwandte Systemmodelle'', Berlin, 10.–11. Oktober 1994, pages 80–83. Forschungsberichte, Bericht 309, Institut für Angewandte Informatik und Formale Beschreibungsverfahren, Universität Karlsruhe (TH), Germany, 1994.

Abstract:

On-the-fly verification of a property means that the property is verified during state space generation, in contrary to the traditional approach where properties are verified after state space generation. As soon as it is known whether the property holds, the generation of the state space can be stopped. Since an erroneous system can have a much larger state space than the intended correct system, it is important to find errors as soon as possible. On the other hand, even in the case that all states become generated, the overhead caused by on-the-fly verification, compared to non-on-the-fly verification, is often negligible.

It has turned out that many of the methods that have originally been designed to avoid the generation of all states in non-on-the fly verification can be applied to on-the-fly verification as well. Valmari's stubborn set method is one such method.

In this paper we describe how the Pr/T-net reachability analysis tool PROD verifies properties on-the-fly.

Keywords:

predicate/transition nets, reachability analysis, on-the-fly verification, linear time temporal properties, stubborn set method

Suggested BibTeX entry:

@inproceedings{VarpaaniemiKimmo-Vrp94c,
    author = {Kimmo Varpaaniemi},
    booktitle = {{A}lgorithmen und {W}erkzeuge f{\"{u}}r {P}etrinetze: {W}orkshop der {G}{I}-{F}achgruppe 0.0.1, ``{P}etrinetze und verwandte {S}ystemmodelle'', {B}erlin, 10.--11. {O}ktober 1994},
    editor = {J{\"{o}}rg Desel and Andreas Oberweis and Wolfgang Reisig},
    pages = {80--83},
    publisher = {Forschungsberichte, Bericht 309, Institut f{\"{u}}r Angewandte Informatik und Formale Beschreibungsverfahren, Universit{\"{a}}t Karlsruhe (TH), Germany},
    title = {{O}n-the-Fly Verification with {P}{R}{O}{D}},
    year = {1994},
}