Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation
This article presents a method for the analysis and verification of Use Case Maps (UCM) models with scenario control structures — protected components and failure handling constructs. UCM models are analyzed and verified with the help of coloured Petri nets (CPN) and the SPIN model checker. Algorithms...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2016-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/407 |
| _version_ | 1797877856414466048 |
|---|---|
| author | N. V. Vizovitin V. A. Nepomniaschy A. A. Stenenko |
| author_facet | N. V. Vizovitin V. A. Nepomniaschy A. A. Stenenko |
| author_sort | N. V. Vizovitin |
| collection | DOAJ |
| description | This article presents a method for the analysis and verification of Use Case Maps (UCM) models with scenario control structures — protected components and failure handling constructs. UCM models are analyzed and verified with the help of coloured Petri nets (CPN) and the SPIN model checker. Algorithms for translating UCM scenario control structures into CPN and CPN into SPIN input language Promela are described. The number of elements of the resulting CPN model and the number of Promela model states are estimated. The presented algorithm and the verification process are illustrated by the study of a network router firmware update. |
| first_indexed | 2024-04-10T02:23:49Z |
| format | Article |
| id | doaj.art-1e89b2d93a0a40ce8c5be7d28d3fb5af |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:23:49Z |
| publishDate | 2016-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-1e89b2d93a0a40ce8c5be7d28d3fb5af2023-03-13T08:07:34ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172016-12-0123668870210.18255/1818-1015-2016-6-688-702336Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM NotationN. V. Vizovitin0V. A. Nepomniaschy1A. A. Stenenko2Институт систем информатики им. А.П. Ершова СО РАНИнститут систем информатики им. А.П. Ершова СО РАНИнститут систем информатики им. А.П. Ершова СО РАНThis article presents a method for the analysis and verification of Use Case Maps (UCM) models with scenario control structures — protected components and failure handling constructs. UCM models are analyzed and verified with the help of coloured Petri nets (CPN) and the SPIN model checker. Algorithms for translating UCM scenario control structures into CPN and CPN into SPIN input language Promela are described. The number of elements of the resulting CPN model and the number of Promela model states are estimated. The presented algorithm and the verification process are illustrated by the study of a network router firmware update.https://www.mais-journal.ru/jour/article/view/407верификациятрансляциянотация use case mapsраскрашенные сети петриверификатор spinзащищенный компонентобработка ошибок |
| spellingShingle | N. V. Vizovitin V. A. Nepomniaschy A. A. Stenenko Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation Моделирование и анализ информационных систем верификация трансляция нотация use case maps раскрашенные сети петри верификатор spin защищенный компонент обработка ошибок |
| title | Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation |
| title_full | Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation |
| title_fullStr | Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation |
| title_full_unstemmed | Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation |
| title_short | Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation |
| title_sort | application of coloured petri nets for verification of scenario control structures in ucm notation |
| topic | верификация трансляция нотация use case maps раскрашенные сети петри верификатор spin защищенный компонент обработка ошибок |
| url | https://www.mais-journal.ru/jour/article/view/407 |
| work_keys_str_mv | AT nvvizovitin applicationofcolouredpetrinetsforverificationofscenariocontrolstructuresinucmnotation AT vanepomniaschy applicationofcolouredpetrinetsforverificationofscenariocontrolstructuresinucmnotation AT aastenenko applicationofcolouredpetrinetsforverificationofscenariocontrolstructuresinucmnotation |