loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
International Conference on Parallel Computing in Electrical Engineering (PARELEC'02)
Verification of Distributed Systems Modelled by High-Level Petri Nets
Warsaw, Poland
September 22-September 25
ISBN: 0-7695-1730-7
ASCII Text
x 
 
V. E. Kozura, V. A. Nepomniaschy, R. M. Novikov, "Verification of Distributed Systems Modelled by High-Level Petri Nets," Parallel Computing in Electrical Engineering, International Conference on, pp. 61, International Conference on Parallel Computing in Electrical Engineering (PARELEC'02), 2002.
 
 
BibTex
x
 
@article{ 10.1109/PCEE.2002.1115202,
author = {V. E. Kozura and V. A. Nepomniaschy and R. M. Novikov},
title = {Verification of Distributed Systems Modelled by High-Level Petri Nets},
journal ={Parallel Computing in Electrical Engineering, International Conference on},
volume = {0},
year = {2002},
isbn = {0-7695-1730-7},
pages = {61},
doi = {http://doi.ieeecomputersociety.org/10.1109/PCEE.2002.1115202},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Parallel Computing in Electrical Engineering, International Conference on
TI - Verification of Distributed Systems Modelled by High-Level Petri Nets
SN - 0-7695-1730-7
SP
EP
A1 - V. E. Kozura,
A1 - V. A. Nepomniaschy,
A1 - R. M. Novikov,
PY - 2002
KW - null
VL - 0
JA - Parallel Computing in Electrical Engineering, International Conference on
ER -
 
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 [7]. An ineffectiveness of the ring protocol is proven by the experiment, and a modified effective ring protocol is verified too.
Citation:
V. E. Kozura, V. A. Nepomniaschy, R. M. Novikov, "Verification of Distributed Systems Modelled by High-Level Petri Nets," parelec, pp.61, International Conference on Parallel Computing in Electrical Engineering (PARELEC'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.