A method to analyze high level petri nets using SPIN model checker Conference

Alam, DMM, He, X. (2017). A method to analyze high level petri nets using SPIN model checker . Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE, 161-166. 10.18293/SEKE2017-162

cited authors

  • Alam, DMM; He, X

abstract

  • High level Petri nets (HLPNs) are a formal method for studying concurrent and distributed systems and have been widely used in many application domains. However, their strong expressive power hinds their analyzability. In this paper, we present a new transformational analysis method for analyzing a special class of HLPNs - predicate transition (PrT) nets. This method extends and improves our prior results by covering more PrT net features including full first order logic formulas and exploring additional alternative translation schemes. This new analysis method is supported by a tool chain - front end PIPE+ for creating and simulating PrT nets and back end SPIN for model checking safety and liveness properties. We have applied this method to two benchmark systems used in annual Petri net model checking contest 2015. We discuss several properties and show the detailed model checking results of two properties in one system.

authors

publication date

  • January 1, 2017

published in

Digital Object Identifier (DOI)

start page

  • 161

end page

  • 166