International Conference on Parallel Computing in Electrical Engineering (PARELEC'02) (2002)
Sept. 22, 2002 to Sept. 25, 2002
V. E. Kozura , Sibirian Division of the Russian Academy of Sciences
V. A. Nepomniaschy , Sibirian Division of the Russian Academy of Sciences
R. M. Novikov , Sibirian Division of the Russian Academy of Sciences
A tool PNV (Petri net verifier) designed for analysis, modelling and verification of coloured Petri nets (CPN) is presented in the paper. The tool consists of two main components: a translator which generates an internal form of CPN and a C++ program modelling the input CPN, and a model-checking component which is applied to CPN limited by finite state systems when properties are presented in mu-calculus. Moreover, the translator generates a program in Pascal extended by a nondeterministic construct in order to model and verify the input CPN. The model-checking component uses the internal form of CPN and includes a model constructor which generates the reachability graph of CPN, and a model-checker. The paper describes a model-checking experiment with CPN which model the ring communication protocol . An ineffectiveness of the ring protocol is proven by the experiment, and a modified effective ring protocol is verified too.
V. A. Nepomniaschy, V. E. Kozura and R. M. Novikov, "Verification of Distributed Systems Modelled by High-Level Petri Nets," International Conference on Parallel Computing in Electrical Engineering (PARELEC'02)(PARELEC), Warsaw, Poland, 2002, pp. 61.