MFDTE/PNTOOL - A TOOL FOR THE RIGOROUS DESIGN, ANALYSIS AND DEVELOPMENT OF CONCURRENT AND TIME-CRITICAL SYSTEMS
Dmitry A. Zaitsev · 2007
SUMMARY This paper describes the PNtool - a tool for a design, analysis and development of concurrent and time-critical systems based on the Petri nets (PN) formalism. The PNtool supports four Petri nets dialects, which are also described in the paper: Generalized Petri nets, Time-basic nets, Evaluative and Coloured Petri nets. The Generalized PN are the basic type of Petri nets supported in the PNtool. Time-basic nets allow to model time-critical systems and Evaluative PN have the computational power equal to the Turing machines. In Coloured Petri nets it is possible to distinguish between tokens, because each of them has a value, called colour. The PNtool allows to design and simulate a system using any of supported PN dialects. In addition, an invariants-based analysis and reachability analysis is available for Generalized PN. Each Generalized and Evaluative PN can be loaded from and saved in a standard interchange format called PNML. All of these features are described in the paper, too. The PNtool is implemented in Java as a part of the mFDT Environment (mFDTE). The mFDTE is a toolset for the formal design and analysis of concurrent discrete and time-critical systems, developed at the home institution of the authors. It integrates three formal methods with complementary features: Petri nets, process algebra and B-Method. This paper also describes interfaces, which connect the PNtool with other parts of mFDTE. The work presented is supported by the grants No. 1/3140/06 and No. 1/4073/07 of the VEGA- The Scientific Grant Agency of Slovakia and NATO CLG 96128 grant.