RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Model. Anal. Inform. Sist., 2014, Volume 21, Number 6, Pages 94–106 (Mi mais415)  

This article is cited in 1 scientific paper (total in 1 paper)

Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets

S. A. Chernenok, V. A. Nepomniaschy

A. P. Ershov Institute of Informatics Systems, Acad. Lavrentjev pr., 6, Novosibirsk 630090, Russia

Abstract: 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.

Keywords: specification, translation, verification, distributed systems, communication protocols, MSC diagrams, Coloured Petri Nets.

Full text: PDF file (206 kB)
References: PDF file   HTML file
UDC: 519.681.3
Received: 12.10.2014

Citation: S. A. Chernenok, V. A. Nepomniaschy, “Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets”, Model. Anal. Inform. Sist., 21:6 (2014), 94–106

Citation in format AMSBIB
\Bibitem{CheNep14}
\by S.~A.~Chernenok, V.~A.~Nepomniaschy
\paper Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets
\jour Model. Anal. Inform. Sist.
\yr 2014
\vol 21
\issue 6
\pages 94--106
\mathnet{http://mi.mathnet.ru/mais415}


Linking options:
  • http://mi.mathnet.ru/eng/mais415
  • http://mi.mathnet.ru/eng/mais/v21/i6/p94

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    This publication is cited in the following articles:
    1. S. A. Chernenok, V. A. Nepomniaschy, “The application of coloured Petri nets to verification of distributed systems specified by message sequence charts”, Trudy ISP RAN, 27:3 (2015), 197–218  mathnet  crossref  elib
  • Моделирование и анализ информационных систем
    Number of views:
    This page:250
    Full text:86
    References:26

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020