The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts
The language of message sequence charts (MSC) is a popular scenario-based specification language used to describe the interaction of components in distributed systems. However, the methods for validation of MSC diagrams are underdeveloped. This paper describes a method for translation of MSC diagram...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/646 |
| _version_ | 1818063106144731136 |
|---|---|
| author | S. A. Chernenok V. A. Nepomniaschy |
| author_facet | S. A. Chernenok V. A. Nepomniaschy |
| author_sort | S. A. Chernenok |
| collection | DOAJ |
| description | The language of message sequence charts (MSC) is a popular scenario-based specification language used to describe the interaction of components in distributed systems. However, the methods for validation of MSC diagrams are underdeveloped. This paper describes a method for translation of MSC diagrams into coloured Petri nets (CPN). The method is applied to the property verification of these diagrams. The considered set of diagram elements is extended by the elements of UML sequence diagrams and compositional MSC diagrams. The properties of the resulting CPN are analyzed and verified using the known system CPN Tools and the CPN verifier based on the SPIN tool. The application of this method is illustrated with an example. |
| first_indexed | 2024-12-10T14:14:49Z |
| format | Article |
| id | doaj.art-c4229cdd83ca4fdb9368520d7d87618d |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-10T14:14:49Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-c4229cdd83ca4fdb9368520d7d87618d2022-12-22T01:45:22ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0127319721810.15514/ISPRAS-2015-27(3)-14646The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence ChartsS. A. Chernenok0V. A. Nepomniaschy1ИСИ СО РАНИСИ СО РАНThe language of message sequence charts (MSC) is a popular scenario-based specification language used to describe the interaction of components in distributed systems. However, the methods for validation of MSC diagrams are underdeveloped. This paper describes a method for translation of MSC diagrams into coloured Petri nets (CPN). The method is applied to the property verification of these diagrams. The considered set of diagram elements is extended by the elements of UML sequence diagrams and compositional MSC diagrams. The properties of the resulting CPN are analyzed and verified using the known system CPN Tools and the CPN verifier based on the SPIN tool. The application of this method is illustrated with an example.https://ispranproceedings.elpub.ru/jour/article/view/646specificationtranslationverificationdistributed systemscommunication protocolsmessage sequence chartsuml sequence diagramscoloured petri netsspecificationtranslationverificationdistributed systemscommunication protocolsmessage sequence chartsuml sequence diagramscoloured petri nets |
| spellingShingle | S. A. Chernenok V. A. Nepomniaschy The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts Труды Института системного программирования РАН specification translation verification distributed systems communication protocols message sequence charts uml sequence diagrams coloured petri nets specification translation verification distributed systems communication protocols message sequence charts uml sequence diagrams coloured petri nets |
| title | The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts |
| title_full | The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts |
| title_fullStr | The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts |
| title_full_unstemmed | The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts |
| title_short | The Application of Coloured Petri Nets to Verification of Distributed Systems Specified by Message Sequence Charts |
| title_sort | application of coloured petri nets to verification of distributed systems specified by message sequence charts |
| topic | specification translation verification distributed systems communication protocols message sequence charts uml sequence diagrams coloured petri nets specification translation verification distributed systems communication protocols message sequence charts uml sequence diagrams coloured petri nets |
| url | https://ispranproceedings.elpub.ru/jour/article/view/646 |
| work_keys_str_mv | AT sachernenok theapplicationofcolouredpetrinetstoverificationofdistributedsystemsspecifiedbymessagesequencecharts AT vanepomniaschy theapplicationofcolouredpetrinetstoverificationofdistributedsystemsspecifiedbymessagesequencecharts AT sachernenok applicationofcolouredpetrinetstoverificationofdistributedsystemsspecifiedbymessagesequencecharts AT vanepomniaschy applicationofcolouredpetrinetstoverificationofdistributedsystemsspecifiedbymessagesequencecharts |