In: Proceedings of the 12th International Conference on Application and Theory of Petri Nets, 1991, Gjern, Denmark, pages 310-328. June 1991.
Abstract: The author presents methods for examining the correctness of programmable logic controllers with the aid of high-level Petri nets. The author has modeled a real application with a high-level Petri net analysis tool (PRENA). The author was able to ascertain the correctness of the system in terms of reactivity to external signals and formulate a correctness criterion in terms of the structure of the reachability graph. Several moleling methods are developed to reduce the size of the reachablility graph.
Keywords: verification (of) programmable logic controller program; high-level net analysis tool, PRENA; reactivity (to) external signal(s); reachability graph reduction.