PIPE+Verifier - A tool for analyzing high level Petri nets Conference

Liu, S, He, X. (2015). PIPE+Verifier - A tool for analyzing high level Petri nets . 2015-January 575-580. 10.18293/SEKE2015-060

cited authors

  • Liu, S; He, X

authors

abstract

  • High level Petri nets (HLPNs) have been widely used to model complex systems; however, their high expressive power costs their analyzability. Model checking techniques have been exploited in analyzing high level Petri nets, but have limited success due to either undecidability problem or state explosion problem. Bounded model checking (BMC) is a promising analysis method that explores state space within a predefined bound. BMC sacrifices the completeness of traditional model checking but becomes more practical and often effective to analyze large models. In our prior work, we have developed a method based on BMC and a supporting tool PIPE+Verifier to analyze high level Petri nets using a state of the art satisfiability modulo theories (SMT) solver Z3 as the backend engine. Our experiment results have been very encouraging. In this paper, we present the design, implementation, and use of PIPE+Verifier, as well as show additional improvements to make PIPE+Verifier more efficient.

publication date

  • January 1, 2015

Digital Object Identifier (DOI)

International Standard Book Number (ISBN) 10

start page

  • 575

end page

  • 580

volume

  • 2015-January