A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems

Abstract

Annotation. In this paper we deal with the PNtool - a tool for a design, analysis and development of concurrent and time-critical systems specified using the Petri nets (PN) formalism. The PNtool supports four Petri nets dialects: Generalized Petri nets, Time-basic nets, Evaluative and Coloured Petri nets. The tool allows to design and simulate a system using any of the supported PN dialects and to perform an invariants-based analysis and reachability analysis for Generalized PN. Each Generalized and Evaluative PN can be also loaded from and saved in a standard interchange format called PNML. The tool 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 982698 grant.В статье идёт речь о проґраммном средстве – PNtool, предназначенным для синтеза и анализа параллельных и критических во времени систем, которые описываются с помощью формализма сетей Петри (СП). PNtool предназначен для поддержки четырёх диалоґов СП: обобщённые СП (generalized PN), временно- базисные СП (Time-basic PN), эвалюационные СП (evaluative PN) и раскрашенные СП (Coloured PN). PNtool позволяет конструирование и симуляцию системы с применением любоґо из упомянутых диалектов СП и также проделать анализ системы с целью одержания её инвариантов , и решения проблемы достижимости для системы представленной обобщённой СП.Спецификация систем на языке обобщённых, или эвалюационных СП может быть представлена и сохраняться в формате PNML.PNtool реализован на языке JAVA, как одна из частей проґраммной среды mFDTE (multi FDT Environment). Среда mFDTE предназначена для синтеза и анализа параллельных (concurrent) дискретных систем , включая и временно-критические системы. Проґраммная среда mFDTE создана в університете авторов статьи. В ней интеґрированы три формальных метода, которые обладают взаимно-комплементарными свойствами: СП, процессные алґебры и метод B AMN. В статье описываются интерфейсы связывающие PNtool с остальными частями среды mFDTE. Результаты исследований представленные в статье были достиґнуты при поддержке грантов № 1/3140/06 , № 1/4073/07 VEGA – научного грантового агентства Словакии, и гранта NATO CLG 982698.