maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2016-6-688-702mais-407Research ArticleОригинальные статьиArticlesПрименение раскрашенных сетей Петри для верификации конструкций управления сценариями языка UCMApplication of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notationhttps://orcid.org/0000-0001-7420-2711ВизовитинН. В.VizovitinN. V.

младший научный сотрудник, проспект Академика Лаврентьева, 6, г. Новосибирск, 630090 Россия

junior researcher, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia

vizovitin@gmail.comhttps://orcid.org/0000-0003-1364-5281НепомнящийВ. А.NepomniaschyV. A.

канд. физ.-мат. наук, доцент, проспект Академика Лаврентьева, 6, г. Новосибирск, 630090 Россия

PhD, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia

vnep@iis.nsk.suhttps://orcid.org/0000-0002-9538-6887СтененкоА. А.StenenkoA. A.

аспирант, проспект Академика Лаврентьева, 6, г. Новосибирск, 630090 Россия

graduate student, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia

stirpar@mail.ruИнститут систем информатики им. А.П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of SciencesRussian Federation201620122016236688702Copyright © Визовитин Н.В., Непомнящий В.А., Стененко А.А., 20162016Визовитин Н.В., Непомнящий В.А., Стененко А.А.Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/407

В данной работе представлен метод анализа и верификации моделей Use Case Maps (UCM) с конструкциями управления сценариями 뜨 защищенными компонентами и конструкциями обработки ошибок. Анализ и верификация UCM моделей проводится с помощью раскрашенных сетей Петри (РСП) и верификатора SPIN. Приводятся описания алгоритмов трансляции UCM в РСП и РСП во входной язык Promela системы SPIN. Впервые представлены оценки для количества элементов результирующих РСП моделей в зависимости от количества элементов исходных UCM моделей с конструкциями управления сценариями, а также количества состояний Promela моделей. Представленный метод анализа и верификации демонстрируется на примере верификации программы обновления прошивки маршрутизатора.

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.

верификациятрансляциянотация Use Case Mapsраскрашенные сети Петриверификатор SPINзащищенный компонентобработка ошибокverificationtranslationUCMcoloured Petri netsSPINprotected componenterror handlingReferencesАнуреев И.С., Баранов С.Н., Белоглазов Д.М., Бодин Е.В., Дробинцев П.Д., Колчин А.В., Котляров В.П., Летичевский А.А., Летичевский А.А. мл., Непомнящий В.А., Никифоров И.В., Потиенко С.В., Прийма Л.В., Тютин Б.В., “Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений”, Тр. СПИИРАН, 26 (2013), 349–383.Anureev I.S., Baranov S.N., Beloglazov D.M., Bodin E.V., Drobitsev P.D., Kolchin A.V., Kotlyarov V.P., Letichevsky A.A., Letichevsky A.A. jr., Nepomniaschy V.A., Nikiforov I.V., Potiyenko S.V., Priyma L.V., Tyutin B.V., “Tools of Integrated Technology for Analysis and Verication of Telecom Application Specs”, SPIIRAS Proceedings, 26 (2013), 349–383, in Russian.Стененко А.А., Непомнящий В.А., Верификация раскрашенных сетей Петри методом проверки моделей, Препринт 178, http://www.iis.nsk.su/files/preprints/stenenko_nepomniaschy_178.pdf, Ин-т систем информатики СО РАН, Новосибирск, 2015, 28 с.Stenenko A.A., Nepomniaschy V.A., Model Checking Approach to Verifiaction of Coloured Petri Nets, Preprint 178, http://www.iis.nsk.su/files/preprints/stenenko_nepomniaschy_178.pdf, Institute of Infornatics Systems RAS, Novosibirsk, 2015, 28 pp., in Russian.Визовитин Н.В., Непомнящий В.А., Алгоритмы трансляции UCM-спецификаций в раскрашенные сети Петри, Препринт 168, http://www.iis.nsk.su/files/preprints/168.pdf, Ин-т систем информатики СО РАН, Новосибирск, 2012, 55 с.Vizovitin N.V., Nepomniaschy V.A., UCM-Specifications to Colored Petri Nets Translation Algotithms, Preprint 168, http://www.iis.nsk.su/files/preprints/168. pdf, Institute of Infornatics Systems RAS, Novosibirsk, 2012, 55 pp., in Russian.Kotlyarov V., Weigert T., “Verifiable Coverage Criteria for Automated Testing”, SDL 2011, LNSC 7083, 2011, 79–89.Kotlyarov V., Weigert T., “Verifiable Coverage Criteria for Automated Testing”, SDL 2011, LNSC 7083, 2011, 79–89.Baranov S.N., Drobintsev P.D., Kotlyarov V.P., Letichevsky A.A., “The Technology of Automated Verification and Testing in Industrial Projects”, Proc. IEEE Russia Northwest Section, 110 Anniversary of Radio Invention Conference, IEEE Press, St.Petersburg, 2005, 81–89.Baranov S.N., Drobintsev P.D., Kotlyarov V.P., Letichevsky A.A., “The Technology of Automated Verification and Testing in Industrial Projects”, Proc. IEEE Russia Northwest Section, 110 Anniversary of Radio Invention Conference, IEEE Press, St.Petersburg, 2005, 81–89.Boulet P., Amyot D., Stepien B., “Towards the Generation of Tests in the Test Description Language from Use Case Map Models”, SDL 2015, LNCS 9369, Springer, 2015, 193–201.Boulet P., Amyot D., Stepien B., “Towards the Generation of Tests in the Test Description Language from Use Case Map Models”, SDL 2015, LNCS 9369, Springer, 2015, 193–201.CPN Tools Homepage, http://cpntools.org/.CPN Tools Homepage, http://cpntools.org/.Hassine J., Rilling J., Dssouli R., “Abstract Operational Semantics for Use Case Maps”, FORTE 2005, LNCS 3731, 2005, 366–380.Hassine J., Rilling J., Dssouli R., “Abstract Operational Semantics for Use Case Maps”, FORTE 2005, LNCS 3731, 2005, 366–380.Hassine J. Early modeling and validation of timed system requirements using Timed Use Case Maps, Requirements Engineering, 20:2 (2015), 181–211.Hassine J. Early modeling and validation of timed system requirements using Timed Use Case Maps, Requirements Engineering, 20:2 (2015), 181–211.Hassine J., Rilling J., Dssouli R, “Use Case Maps as a Property Specification Language”, Software and Systems Modeling, 8:2 (2009), 205–220.Hassine J., Rilling J., Dssouli R, “Use Case Maps as a Property Specification Language”, Software and Systems Modeling, 8:2 (2009), 205–220.Holzmann G.J, The SPIN model checker. Primer and Reference Manual, Addison-Wesley, 2004.Holzmann G.J, The SPIN model checker. Primer and Reference Manual, Addison-Wesley, 2004.ITU-T, Recommendation Z.151 (10/12), User Requirements Notation (URN) — Language definition, http://www.itu.int/rec/T-REC-Z.151/en.ITU-T, Recommendation Z.151 (10/12), User Requirements Notation (URN) — Language definition, http://www.itu.int/rec/T-REC-Z.151/en.jUCMNav — Eclipse plugin for the User Requirements Notation, http://jucmnav.softwareengineering.ca/ucm/bin/view/ProjetSEG/WebHome.jUCMNav — Eclipse plugin for the User Requirements Notation, http://jucmnav.softwareengineering.ca/ucm/bin/view/ProjetSEG/WebHome.Jensen K., Kristensen L.M, Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Springer, 2009.Jensen K., Kristensen L.M, Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Springer, 2009.Vizovitin N.V., Application of coloured Petri nets for verification of scenario control structures in UCM notation. Appendix, http://bitbucket.org/vizovitin/ucm-verification- examples-3.Vizovitin N.V., Application of coloured Petri nets for verification of scenario control structures in UCM notation. Appendix, http://bitbucket.org/vizovitin/ucm-verification- examples-3.Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A., “Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets”, Cybernetics and Sys. Anal., 51:2 (2015), 213– 222.Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A., “Verifying UCM Specifications of Distributed Systems Using Colored Petri Nets”, Cybernetics and Sys. Anal., 51:2 (2015), 213– 222.Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A., “Verification of UCM Models with Scenario Control Structures Using Colored Petri Nets”, System Informatics, 7 (2016), 11–22.Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A., “Verification of UCM Models with Scenario Control Structures Using Colored Petri Nets”, System Informatics, 7 (2016), 11–22.

The authors declare that there are no conflicts of interest present.