Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри
Представлена новая система анализа и верификации Use Case Maps (UCM) спецификаций с использованием раскрашенных сетей Петри и системы верификации SPIN. Стандартизованная нотация UCM удобное графическое средство формального описания функциональных требований. Описаны алгоритмы трансляции UCM-специфик...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2015 |
| Автори: | , , |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2015
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/124777 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри / Н.В. Визовитин, В.А. Непомнящий, А.А. Стененко // Кибернетика и системный анализ. — 2015. — Т. 51, № 2. — С. 62-74. — Бібліогр.: 17 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862688944333783040 |
|---|---|
| author | Визовитин, Н.В. Непомнящий, В.А. Стененко, А.А. |
| author_facet | Визовитин, Н.В. Непомнящий, В.А. Стененко, А.А. |
| citation_txt | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри / Н.В. Визовитин, В.А. Непомнящий, А.А. Стененко // Кибернетика и системный анализ. — 2015. — Т. 51, № 2. — С. 62-74. — Бібліогр.: 17 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| 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.
|
| first_indexed | 2025-12-07T16:09:52Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-124777 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T16:09:52Z |
| publishDate | 2015 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| 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 |
| spellingShingle | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри Визовитин, Н.В. Непомнящий, В.А. Стененко, А.А. Кибернетика |
| title | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри |
| title_alt | Верифікація UCM-специфікацій розподілених систем з використанням розфарбованих мереж Петрі Verifying UCM-specifications of distributed systems using colored Petri nets |
| title_full | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри |
| title_fullStr | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри |
| title_full_unstemmed | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри |
| title_short | Верификация UCM-спецификаций распределенных систем с использованием раскрашенных сетей Петри |
| title_sort | верификация ucm-спецификаций распределенных систем с использованием раскрашенных сетей петри |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/124777 |
| 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 |