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...
Saved in:
| Date: | 2008 |
|---|---|
| Main Authors: | , , |
| 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 |