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


https://doi.org/10.18255/1818-1015-2016-6-688-702

Полный текст:


Аннотация

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


Об авторах

Н. В. Визовитин
Институт систем информатики им. А.П. Ершова СО РАН
Россия

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



В. А. Непомнящий
Институт систем информатики им. А.П. Ершова СО РАН
Россия

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



А. А. Стененко
Институт систем информатики им. А.П. Ершова СО РАН
Россия

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



Список литературы

1. Ануреев И.С., Баранов С.Н., Белоглазов Д.М., Бодин Е.В., Дробинцев П.Д., Колчин А.В., Котляров В.П., Летичевский А.А., Летичевский А.А. мл., Непомнящий В.А., Никифоров И.В., Потиенко С.В., Прийма Л.В., Тютин Б.В., “Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений”, Тр. СПИИРАН, 26 (2013), 349–383.

2. Стененко А.А., Непомнящий В.А., Верификация раскрашенных сетей Петри методом проверки моделей, Препринт 178, http://www.iis.nsk.su/files/preprints/stenenko_nepomniaschy_178.pdf, Ин-т систем информатики СО РАН, Новосибирск, 2015, 28 с.

3. Визовитин Н.В., Непомнящий В.А., Алгоритмы трансляции UCM-спецификаций в раскрашенные сети Петри, Препринт 168, http://www.iis.nsk.su/files/preprints/168.pdf, Ин-т систем информатики СО РАН, Новосибирск, 2012, 55 с.

4. Kotlyarov V., Weigert T., “Verifiable Coverage Criteria for Automated Testing”, SDL 2011, LNSC 7083, 2011, 79–89.

5. 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.

6. 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.

7. CPN Tools Homepage, http://cpntools.org/.

8. Hassine J., Rilling J., Dssouli R., “Abstract Operational Semantics for Use Case Maps”, FORTE 2005, LNCS 3731, 2005, 366–380.

9. Hassine J. Early modeling and validation of timed system requirements using Timed Use Case Maps, Requirements Engineering, 20:2 (2015), 181–211.

10. Hassine J., Rilling J., Dssouli R, “Use Case Maps as a Property Specification Language”, Software and Systems Modeling, 8:2 (2009), 205–220.

11. Holzmann G.J, The SPIN model checker. Primer and Reference Manual, Addison-Wesley, 2004.

12. ITU-T, Recommendation Z.151 (10/12), User Requirements Notation (URN) — Language definition, http://www.itu.int/rec/T-REC-Z.151/en.

13. jUCMNav — Eclipse plugin for the User Requirements Notation, http://jucmnav.softwareengineering.ca/ucm/bin/view/ProjetSEG/WebHome.

14. Jensen K., Kristensen L.M, Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Springer, 2009.

15. 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.

16. 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.

17. 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.


Дополнительные файлы

Для цитирования: Визовитин Н.В., Непомнящий В.А., Стененко А.А. Применение раскрашенных сетей Петри для верификации конструкций управления сценариями языка UCM. Моделирование и анализ информационных систем. 2016;23(6):688-702. https://doi.org/10.18255/1818-1015-2016-6-688-702

For citation: Vizovitin N.V., Nepomniaschy V.A., Stenenko A.A. Application of Coloured Petri Nets for Verification of Scenario Control Structures in UCM Notation. Modeling and Analysis of Information Systems. 2016;23(6):688-702. (In Russ.) https://doi.org/10.18255/1818-1015-2016-6-688-702

Просмотров: 358

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)