Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри

Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри

Представлена новая система анализа и верификации Use Case Maps (UCM) спецификаций с использованием раскрашенных сетей Петри и системы верификации SPIN. Стандартизованная нотация UCM удобное графическое средство формального описания функциональных требований. Описаны алгоритмы трансляции UCM-специфик...

Ausführliche Beschreibung

Gespeichert in:
Bibliographische Detailangaben
Veröffentlicht in:Кибернетика и системный анализ
Datum:2015
Hauptverfasser: Визовитин, Н.В., Непомнящий, В.А., Стененко, А.А.
Format: Artikel
Sprache:Russian
Veröffentlicht: Інститут кібернетики ім. В.М. Глушкова НАН України 2015
Schlagworte:
Кибернетика
Online Zugang:https://nasplib.isofts.kiev.ua/handle/123456789/124777
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри / Н.В. Визовитин, В.А. Непомнящий, А.А. Стененко // Кибернетика и системный анализ. — 2015. — Т. 51, № 2. — С. 62-74. — Бібліогр.: 17 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-124777
record_format dspace
spelling Визовитин, Н.В.
Непомнящий, В.А.
Стененко, А.А.
2017-10-05T06:23:46Z
2017-10-05T06:23:46Z
2015
Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри / Н.В. Визовитин, В.А. Непомнящий, А.А. Стененко // Кибернетика и системный анализ. — 2015. — Т. 51, № 2. — С. 62-74. — Бібліогр.: 17 назв. — рос.
0023-1274
https://nasplib.isofts.kiev.ua/handle/123456789/124777
519.172
Представлена новая система анализа и верификации Use Case Maps (UCM) спецификаций с использованием раскрашенных сетей Петри и системы верификации SPIN. Стандартизованная нотация UCM удобное графическое средство формального описания функциональных требований. Описаны алгоритмы трансляции UCM-спецификаций в раскрашенные сети Петри, а также трансляции последних во входной язык Promela системы SPIN. Приведен вывод оценки сложности получаемых раскрашенных сетей Петри. Работа представленных алгоритмов и инструментов демонстрируется на примере верификации коммуникационного протокола с локализацией и исправлением ошибок в исходной UCM-спецификации.
Представлено нову систему аналізу і верифікації Use Case Maps (UCM) специфікацій розфарбованих мереж Петрі та системи верифікації SPIN. Стандартизована нотація UCM зручний графічний засіб формального опису функціональних вимог. Описано алгоритми трансляції UCM-специфікацій в розфарбованій мережі Петрі, а також їх трансляцію у вихідну мову Promela системи SPIN. Зроблено висновок щодо оцінки складності отриманих розфарбованих мереж Петрі. Роботу наведених алгоритмів та інструментів показано на прикладі верифікації комунікаційного протоколу з локалізацією та виправленням помилок в початковій UCM-специфікації.
A new method for analysis and verification of Use Case Maps (UCM) specifications with the help of colored Petri nets and SPIN model checker is presented. Standardized UCM notation is a convenient visual language that allows formal expression of functional requirements. Algorithms for translation of UCM-specifications into colored Petri nets and colored Petri nets into input language Promela of the SPIN model checker are described. The complexity of the derived colored Petri nets is evaluated. We demonstrate the application of the translation algorithms and developed toolset in a case study. A simple network protocol is corrected and verified after several errors have been found in the source UCM-specification.
ru
Інститут кібернетики ім. В.М. Глушкова НАН України
Кибернетика и системный анализ
Кибернетика
Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
Верифікація UCM-специфікацій розподілених систем з використанням розфарбованих мереж Петрі
Verifying UCM-specifications of distributed systems using colored Petri nets
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
spellingShingle Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
Визовитин, Н.В.
Непомнящий, В.А.
Стененко, А.А.
Кибернетика
title_short Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
title_full Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
title_fullStr Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
title_full_unstemmed Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
title_sort верификация ucm-спецификаций распределенных систем с использованием раскрашенных сетей петри
author Визовитин, Н.В.
Непомнящий, В.А.
Стененко, А.А.
author_facet Визовитин, Н.В.
Непомнящий, В.А.
Стененко, А.А.
topic Кибернетика
topic_facet Кибернетика
publishDate 2015
language Russian
container_title Кибернетика и системный анализ
publisher Інститут кібернетики ім. В.М. Глушкова НАН України
format Article
title_alt Верифікація UCM-специфікацій розподілених систем з використанням розфарбованих мереж Петрі
Verifying UCM-specifications of distributed systems using colored Petri nets
description Представлена новая система анализа и верификации Use Case Maps (UCM) спецификаций с использованием раскрашенных сетей Петри и системы верификации SPIN. Стандартизованная нотация UCM удобное графическое средство формального описания функциональных требований. Описаны алгоритмы трансляции UCM-спецификаций в раскрашенные сети Петри, а также трансляции последних во входной язык Promela системы SPIN. Приведен вывод оценки сложности получаемых раскрашенных сетей Петри. Работа представленных алгоритмов и инструментов демонстрируется на примере верификации коммуникационного протокола с локализацией и исправлением ошибок в исходной UCM-спецификации. Представлено нову систему аналізу і верифікації Use Case Maps (UCM) специфікацій розфарбованих мереж Петрі та системи верифікації SPIN. Стандартизована нотація UCM зручний графічний засіб формального опису функціональних вимог. Описано алгоритми трансляції UCM-специфікацій в розфарбованій мережі Петрі, а також їх трансляцію у вихідну мову Promela системи SPIN. Зроблено висновок щодо оцінки складності отриманих розфарбованих мереж Петрі. Роботу наведених алгоритмів та інструментів показано на прикладі верифікації комунікаційного протоколу з локалізацією та виправленням помилок в початковій UCM-специфікації. A new method for analysis and verification of Use Case Maps (UCM) specifications with the help of colored Petri nets and SPIN model checker is presented. Standardized UCM notation is a convenient visual language that allows formal expression of functional requirements. Algorithms for translation of UCM-specifications into colored Petri nets and colored Petri nets into input language Promela of the SPIN model checker are described. The complexity of the derived colored Petri nets is evaluated. We demonstrate the application of the translation algorithms and developed toolset in a case study. A simple network protocol is corrected and verified after several errors have been found in the source UCM-specification.
issn 0023-1274
url https://nasplib.isofts.kiev.ua/handle/123456789/124777
citation_txt Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри / Н.В. Визовитин, В.А. Непомнящий, А.А. Стененко // Кибернетика и системный анализ. — 2015. — Т. 51, № 2. — С. 62-74. — Бібліогр.: 17 назв. — рос.
work_keys_str_mv AT vizovitinnv verifikaciâucmspecifikaciiraspredelennyhsistemsispolʹzovaniemraskrašennyhseteipetri
AT nepomnâŝiiva verifikaciâucmspecifikaciiraspredelennyhsistemsispolʹzovaniemraskrašennyhseteipetri
AT stenenkoaa verifikaciâucmspecifikaciiraspredelennyhsistemsispolʹzovaniemraskrašennyhseteipetri
AT vizovitinnv verifíkacíâucmspecifíkacíirozpodílenihsistemzvikoristannâmrozfarbovanihmerežpetrí
AT nepomnâŝiiva verifíkacíâucmspecifíkacíirozpodílenihsistemzvikoristannâmrozfarbovanihmerežpetrí
AT stenenkoaa verifíkacíâucmspecifíkacíirozpodílenihsistemzvikoristannâmrozfarbovanihmerežpetrí
AT vizovitinnv verifyingucmspecificationsofdistributedsystemsusingcoloredpetrinets
AT nepomnâŝiiva verifyingucmspecificationsofdistributedsystemsusingcoloredpetrinets
AT stenenkoaa verifyingucmspecificationsofdistributedsystemsusingcoloredpetrinets
first_indexed 2025-12-07T16:09:52Z
last_indexed 2025-12-07T16:09:52Z
_version_ 1850866445506838529

Ähnliche Einträge