maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2014-6-94-106mais-74Research ArticleОригинальные статьиArticlesАнализ и верификация MSC-диаграмм распределённых систем с помощью раскрашенных сетей ПетриAnalysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri NetsЧерненокСергей АнатольевичChernenokS. A.

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

аспирант, Acad. Lavrentjev pr., 6, Novosibirsk 630090, Russia

chernenoksergey@gmail.comНепомнящийВалерий АлександровичNepomniaschyV. A.

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

кандидат физ.-мат. наук, зав. лабораторией, Acad. Lavrentjev pr., 6, Novosibirsk 630090, Russia

vnep@iis.nsk.suИнститут систем информатики имени А. П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics SystemsRussian Federation20142012201421694106Copyright © Черненок С.А., Непомнящий В.А., 20142014Черненок С.А., Непомнящий В.А.Chernenok S.A., Nepomniaschy V.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/74

Стандартный язык диаграмм последовательных сообщений MSC предназначен для описания сценариев взаимодействия объектов. Благодаря своей выразительности и простоте MSC-диаграммы широко применяются на практике на всех этапах проектирования и разработки программных систем. В частности, язык MSC используется для спецификации поведения в распределенных системах и коммуникационных протоколах. В работе рассматривается метод анализа и верификации диаграмм MSC и HMSC. Метод основывается на трансляции конструкций (H)MSC в раскрашенные сети Петри. Описываемые правила трансляции охватывают большинство конструкций стандарта, включая концепцию данных. Приводятся оценки размера сетей Петри, полученных в результате трансляции. Свойства построенных сетей анализируются и верифицируются с помощью известной системы CPN Tools и системы автоматической верификации на основе SPIN. Работоспособность данного метода продемонстрирована на примере.

The standard language of message sequence charts MSC is intended to describe scenarios of object interaction. Due to their expressiveness and simplicity MSC diagrams are widely used in practice at all stages of system design and development. In particular, the MSC language is used for describing communication behavior in distributed systems and communication protocols. In this paper the method for analysis and verification of MSC and HMSC diagrams is considered. The method is based on the translation of (H)MSC into coloured Petri nets. The translation algorithms cover most standard elements of the MSC including data concepts. Size estimates of the CPN which is the result of the translation are given. Properties of the resulting CPN are analyzed and verified by using the known system CPN Tools and the CPN verifier based on the known tool SPIN. The translation method has been demonstrated by the example.

спецификациятрансляцияверификацияраспределённые системытелекоммуникационные протоколыMSC-диаграммыраскрашенные сети Петриspecificationtranslationverificationdistributed systemscommunication protocolsMSC diagramsColoured Petri NetsРФФИReferencesАнуреев И.С., Баранов С.Н., Белоглазов Д.М., Бодин Е.В., Дробинцев П.Д., Колчин А.В., Котляров В.П., Летичевский А.А., Летичевский А.А. мл., Непомнящий В.А., Никифоров И.В., Потиенко С.В., Прийма Л.В., Тютин Б.В. Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений // СПИИРАН. 2013. Вып. 3(26). С. 349–383 (English transl.: Anureev I., Baranov S., Beloglazov D., Bodin E., Drobintsev P., Kolchin A., Kotlyarov V., Letichevsky A., Letichevsky A. Jr., Nepomniaschy V., Nikiforov I., Potienko S., Pryma L., Tyutin B. Tools for Supporting Integrated Technology of Analysis and Verification of Specifications for Telecommunication Applications // SPIIRAS. Proc. 2013. V. 3. P. 349–383.)Ануреев И.С., Баранов С.Н., Белоглазов Д.М., Бодин Е.В., Дробинцев П.Д., Колчин А.В., Котляров В.П., Летичевский А.А., Летичевский А.А. мл., Непомнящий В.А., Никифоров И.В., Потиенко С.В., Прийма Л.В., Тютин Б.В. Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений // СПИИРАН. 2013. Вып. 3(26). С. 349–383 (English transl.: Anureev I., Baranov S., Beloglazov D., Bodin E., Drobintsev P., Kolchin A., Kotlyarov V., Letichevsky A., Letichevsky A. Jr., Nepomniaschy V., Nikiforov I., Potienko S., Pryma L., Tyutin B. Tools for Supporting Integrated Technology of Analysis and Verification of Specifications for Telecommunication Applications // SPIIRAS. Proc. 2013. V. 3. P. 349–383.)Стененко А.А., Непомнящий В.А. Верификация раскрашенных сетей Петри методом проверки моделей / Институт систем информатики СО РАН. Препринт 172. Новосибирск, 2014. http://www.iis.nsk.su/files/preprints/172.pdf (English transl.: Stenenko A.A., Nepomniaschy V.A. Verification of Coloured Petri Nets by model checking method / Institute of Informatics Systems SB RAS. Preprint 172. Novosibirsk, 2014.)Стененко А.А., Непомнящий В.А. Верификация раскрашенных сетей Петри методом проверки моделей / Институт систем информатики СО РАН. Препринт 172. Новосибирск, 2014. http://www.iis.nsk.su/files/preprints/172.pdf (English transl.: Stenenko A.A., Nepomniaschy V.A. Verification of Coloured Petri Nets by model checking method / Institute of Informatics Systems SB RAS. Preprint 172. Novosibirsk, 2014.)Черненок С.А., Непомнящий В.А. Анализ MSC-диаграмм распределенных систем с помощью раскрашенных сетей Петри / Институт систем информатики СО РАН. Препринт 171. Новосибирск, 2013. http://www.iis.nsk.su/files/preprints/171.pdf (English transl.: Chernenok S.A., Nepomniaschy V.A. Analysis of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets / Institute of Informatics Systems SB RAS. Preprint 171. Novosibirsk, 2013.)Черненок С.А., Непомнящий В.А. Анализ MSC-диаграмм распределенных систем с помощью раскрашенных сетей Петри / Институт систем информатики СО РАН. Препринт 171. Новосибирск, 2013. http://www.iis.nsk.su/files/preprints/171.pdf (English transl.: Chernenok S.A., Nepomniaschy V.A. Analysis of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets / Institute of Informatics Systems SB RAS. Preprint 171. Novosibirsk, 2013.)Abdallah R., Gotlieb A., Helouet L., Jard C. Scenario Realizability with Constraint Optimization // FASE 2013, LNCS 7793. 2013. P. 194–209.Abdallah R., Gotlieb A., Helouet L., Jard C. Scenario Realizability with Constraint Optimization // FASE 2013, LNCS 7793. 2013. P. 194–209.Chernenok S.A., Nepomniaschy V.A. Analysis and Verification of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets // Proc. of 5th Workshop "PSSV: Theory and Applications". Moscow, 2014. P. 38–49.Chernenok S.A., Nepomniaschy V.A. Analysis and Verification of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets // Proc. of 5th Workshop "PSSV: Theory and Applications". Moscow, 2014. P. 38–49.Chernenok S.A. Analysis and Verification of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets. Appendix. http://bitbucket.org/chernenok/msc-verificationChernenok S.A. Analysis and Verification of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets. Appendix. http://bitbucket.org/chernenok/msc-verificationEichner C., Fleischhack H., Meyer R., Schrimpf U., Stehno S. Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets // SDL-Forum 2005, LNCS 3530. P. 133–148.Eichner C., Fleischhack H., Meyer R., Schrimpf U., Stehno S. Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets // SDL-Forum 2005, LNCS 3530. P. 133–148.Genest B., Muscholl A., Peled D. Message Sequence Charts // Lectures on Concurrency and Petri Nets, LNCS 3098. 2003. P. 537–558.Genest B., Muscholl A., Peled D. Message Sequence Charts // Lectures on Concurrency and Petri Nets, LNCS 3098. 2003. P. 537–558.ITU-T Recommendation Z.120 (02/2011): Message Sequence Chart (MSC). 2011.ITU-T Recommendation Z.120 (02/2011): Message Sequence Chart (MSC). 2011.Jensen K., Kristensen L.M. Coloured Petri Nets: Modeling and Validation of Concurrent Systems. Springer, 2009.Jensen K., Kristensen L.M. Coloured Petri Nets: Modeling and Validation of Concurrent Systems. Springer, 2009.Kryvyi S., Matvyeyeva L. Algorithm of Translation of MSC-specified System into Petri Net // Fundamenta Informaticae, 2007. V. 79. № 3–4. P. 431–445.Kryvyi S., Matvyeyeva L. Algorithm of Translation of MSC-specified System into Petri Net // Fundamenta Informaticae, 2007. V. 79. № 3–4. P. 431–445.Letichevsky A., Kapitonova J., Letichevsky A. Jr., Volkov V., Baranov S., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Computer Networks: The International Journal of Computer and Telecommunications Networking. 2005. V. 49. № 5. P. 661–675.Letichevsky A., Kapitonova J., Letichevsky A. Jr., Volkov V., Baranov S., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Computer Networks: The International Journal of Computer and Telecommunications Networking. 2005. V. 49. № 5. P. 661–675.Liang H., Dingel J., Diskin Z. A Comparative Survey of Scenario-Based to State-Based Model Synthesis Approaches // SCESM 2006, ACM. NY, 2006. P. 5–12.Liang H., Dingel J., Diskin Z. A Comparative Survey of Scenario-Based to State-Based Model Synthesis Approaches // SCESM 2006, ACM. NY, 2006. P. 5–12.Muccini H. Detecting Implied Scenarios Analyzing Non-local Branching Choices // FASE 2013, LNCS 2621. P. 372–386.Muccini H. Detecting Implied Scenarios Analyzing Non-local Branching Choices // FASE 2013, LNCS 2621. P. 372–386.Ribeiro O.R., Fernandes J.M. Some Rules to Transform Sequence Diagrams into Coloured Petri Nets // 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2006). Aarhus, Denmark, 2006. P. 237–256.Ribeiro O.R., Fernandes J.M. Some Rules to Transform Sequence Diagrams into Coloured Petri Nets // 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2006). Aarhus, Denmark, 2006. P. 237–256.Tanenbaum A. Computers Networks (4th Edition). Prentice Hall PTR, 2002.Tanenbaum A. Computers Networks (4th Edition). Prentice Hall PTR, 2002.Yang N., Yu H., Sun H., Qian Z. Modeling UML sequence diagrams using extended Petri nets // Telecommunication Systems. Springer, 2012. V. 51. № 2–3. P. 147–158.Yang N., Yu H., Sun H., Qian Z. Modeling UML sequence diagrams using extended Petri nets // Telecommunication Systems. Springer, 2012. V. 51. № 2–3. P. 147–158.

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