Title :
Verification of distributed systems modelled by high-level Petri nets
Author :
Kozura, V.E. ; Nepomniaschy, V.A. ; Novikov, R.M.
Author_Institution :
Inst. of Inf. Syst., Acad. of Sci., Novosibirsk, Russia
Abstract :
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 models the ring communication protocol (Cohen and Segall, 1991). An ineffectiveness of the ring protocol is proven by the experiment, and a modified effective ring protocol is verified too.
Keywords :
C++ language; Pascal; Petri nets; distributed processing; formal verification; graph colouring; process algebra; C++ program; CPN; PNV tool; Pascal; coloured Petri nets; distributed systems modelling; distributed systems verification; experiment; finite state systems; high-level Petri nets; model checking; mu-calculus; nondeterministic construct; reachability graph; ring communication protocol; ring protocol; Analytical models; Automata; Computer science; Embedded system; Hardware; Informatics; Petri nets; Protocols; Software design; Software systems;
Conference_Titel :
Parallel Computing in Electrical Engineering, 2002. PARELEC '02. Proceedings. International Conference on
Print_ISBN :
0-7695-1730-7
DOI :
10.1109/PCEE.2002.1115202
