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

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 Petr...

Full description

Saved in:
Bibliographic Details
Date:2008
Main Authors: Hudak, S., Korecko, S., Simonak, S.
Format: Article
Language:English
Published: Інститут програмних систем НАН України 2008
Subjects:
Online Access:https://nasplib.isofts.kiev.ua/handle/123456789/1481
Tags: Add Tag
No Tags, Be the first to tag this record!
Journal Title:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Cite this:A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems / S. Hudak, S. Korecko, S. Simonak // Пробл. програмув. — 2008. — N 2-3. — С. 613-621. — Бібліогр.: 14 назв. — англ.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-1481
record_format dspace
spelling Hudak, S.
Korecko, S.
Simonak, S.
2008-07-31T14:17:25Z
2008-07-31T14:17:25Z
2008
A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems / S. Hudak, S. Korecko, S. Simonak // Пробл. програмув. — 2008. — N 2-3. — С. 613-621. — Бібліогр.: 14 назв. — англ.
1727-4907
https://nasplib.isofts.kiev.ua/handle/123456789/1481
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.
en
Інститут програмних систем НАН України
№2-3
С. 613-621
Інструментальні засоби і середовища програмування
A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
spellingShingle A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
Hudak, S.
Korecko, S.
Simonak, S.
Інструментальні засоби і середовища програмування
title_short A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
title_full A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
title_fullStr A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
title_full_unstemmed A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
title_sort support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems
author Hudak, S.
Korecko, S.
Simonak, S.
author_facet Hudak, S.
Korecko, S.
Simonak, S.
topic Інструментальні засоби і середовища програмування
topic_facet Інструментальні засоби і середовища програмування
publishDate 2008
language English
publisher Інститут програмних систем НАН України
format Article
description 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.
issn 1727-4907
url https://nasplib.isofts.kiev.ua/handle/123456789/1481
citation_txt A Support tool for the reachability and other petri nets- related problems and formal design and analysis of discrete systems / S. Hudak, S. Korecko, S. Simonak // Пробл. програмув. — 2008. — N 2-3. — С. 613-621. — Бібліогр.: 14 назв. — англ.
work_keys_str_mv AT hudaks asupporttoolforthereachabilityandotherpetrinetsrelatedproblemsandformaldesignandanalysisofdiscretesystems
AT koreckos asupporttoolforthereachabilityandotherpetrinetsrelatedproblemsandformaldesignandanalysisofdiscretesystems
AT simonaks asupporttoolforthereachabilityandotherpetrinetsrelatedproblemsandformaldesignandanalysisofdiscretesystems
AT hudaks supporttoolforthereachabilityandotherpetrinetsrelatedproblemsandformaldesignandanalysisofdiscretesystems
AT koreckos supporttoolforthereachabilityandotherpetrinetsrelatedproblemsandformaldesignandanalysisofdiscretesystems
AT simonaks supporttoolforthereachabilityandotherpetrinetsrelatedproblemsandformaldesignandanalysisofdiscretesystems
first_indexed 2025-12-07T21:13:00Z
last_indexed 2025-12-07T21:13:00Z
_version_ 1850885517569163264