Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets
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 com...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2014-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/74 |
| _version_ | 1797877886414225408 |
|---|---|
| author | S. A. Chernenok V. A. Nepomniaschy |
| author_facet | S. A. Chernenok V. A. Nepomniaschy |
| author_sort | S. A. Chernenok |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:25:06Z |
| format | Article |
| id | doaj.art-90a086dd2674476395c6a14bf4c534df |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:25:06Z |
| publishDate | 2014-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-90a086dd2674476395c6a14bf4c534df2023-03-13T08:07:33ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172014-12-012169410610.18255/1818-1015-2014-6-94-10668Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri NetsS. A. Chernenok0V. A. Nepomniaschy1Институт систем информатики имени А. П. Ершова СО РАНИнститут систем информатики имени А. П. Ершова СО РАН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.https://www.mais-journal.ru/jour/article/view/74спецификациятрансляцияверификацияраспределённые системытелекоммуникационные протоколыmsc-диаграммыраскрашенные сети петри |
| spellingShingle | S. A. Chernenok V. A. Nepomniaschy Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets Моделирование и анализ информационных систем спецификация трансляция верификация распределённые системы телекоммуникационные протоколы msc-диаграммы раскрашенные сети петри |
| title | Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets |
| title_full | Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets |
| title_fullStr | Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets |
| title_full_unstemmed | Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets |
| title_short | Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets |
| title_sort | analysis and verification of message sequence charts of distributed systems with the help of coloured petri nets |
| topic | спецификация трансляция верификация распределённые системы телекоммуникационные протоколы msc-диаграммы раскрашенные сети петри |
| url | https://www.mais-journal.ru/jour/article/view/74 |
| work_keys_str_mv | AT sachernenok analysisandverificationofmessagesequencechartsofdistributedsystemswiththehelpofcolouredpetrinets AT vanepomniaschy analysisandverificationofmessagesequencechartsofdistributedsystemswiththehelpofcolouredpetrinets |