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
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.
specification, translation, verification, distributed systems, communication protocols, MSC diagrams, Coloured Petri Nets.
PDF file (206 kB)
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
\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.
Citing articles on Google Scholar:
Related articles on Google Scholar:
This publication is cited in the following articles:
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
|Number of views:|