Geodesic
Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets
Modelirovanie i analiz informacionnyh sistem, Tome 21 (2014) no. 6, pp. 94-106.

Voir la notice de l'article provenant de la source Math-Net.Ru

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, MSC diagrams, Coloured Petri Nets.
Mots-clés : communication protocols 
@article{MAIS_2014_21_6_a8,
     author = {S. A. Chernenok and V. A. Nepomniaschy},
     title = {Analysis and verification of message sequence charts of distributed systems with the help of {Coloured} {Petri} {Nets}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {94--106},
     publisher = {mathdoc},
     volume = {21},
     number = {6},
     year = {2014},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a8/}
}
TY  - JOUR
AU  - S. A. Chernenok
AU  - V. A. Nepomniaschy
TI  - Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2014
SP  - 94
EP  - 106
VL  - 21
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a8/
LA  - ru
ID  - MAIS_2014_21_6_a8
ER  - 
%0 Journal Article
%A S. A. Chernenok
%A V. A. Nepomniaschy
%T Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets
%J Modelirovanie i analiz informacionnyh sistem
%D 2014
%P 94-106
%V 21
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a8/
%G ru
%F MAIS_2014_21_6_a8
S. A. Chernenok; V. A. Nepomniaschy. Analysis and verification of message sequence charts of distributed systems with the help of Coloured Petri Nets. Modelirovanie i analiz informacionnyh sistem, Tome 21 (2014) no. 6, pp. 94-106. http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a8/

[1] I. Anureev, S. Baranov, D. Beloglazov, E. Bodin, P. Drobintsev, A. Kolchin, V. Kotlyarov, A. Letichevsky, A. Jr. Letichevsky, V. Nepomniaschy, I. Nikiforov, S. Potienko, L. Pryma, B. Tyutin, “Tools for Supporting Integrated Technology of Analysis and Verification of Specifications for Telecommunication Applications”, SPIIRAS. Proc., 26 (2013), 349–383

[2] V. E. Kozyura, V. A. Nepomniaschy, R. M. Novikov, Verification of Coloured Petri Nets by model checking method, Preprint 89, Institute of Informatics Systems SB RAS, Novosibirsk, 2001

[3] S.Ȧ. Chernenok, V. A. Nepomniaschy, Analysis of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets, Preprint 171, Institute of Informatics Systems SB RAS, Novosibirsk, 2013

[4] R. Abdallah, A. Gotlieb, L. Helouet, C. Jard, “Scenario Realizability with Constraint Optimization”, FASE 2013, LNCS, 7793, 2013, 194–209

[5] S. A. Chernenok, V. A. Nepomniaschy, “Analysis and Verification of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets”, Proc. of 5th Workshop “PSSV: Theory and Applications” (Moscow, 2014), 38-49

[6] S. A. Chernenok, Analysis and Verification of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets. Appendix, http://bitbucket.org/chernenok/msc-verification

[7] C. Eichner, H. Fleischhack, R. Meyer, U. Schrimpf, S. Stehno, “Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets”, SDL-Forum 2005, LNCS, 3530, 133–148

[8] B. Genest, A. Muscholl, D. Peled, “Message Sequence Charts”, Lectures on Concurrency and Petri Nets, LNCS, 3098, 2003, 537–558 | DOI | MR

[9] ITU-T Recommendation Z.120 (02/2011): Message Sequence Chart (MSC), 2011

[10] K. Jensen, L. M. Kristensen, Coloured Petri Nets: Modeling and Validation of Concurrent Systems, Springer, 2009

[11] S. Kryvyi, L. Matvyeyeva, “Algorithm of Translation of MSC-specified System into Petri Net”, Fundamenta Informaticae, 79:3–4 (2007), 431–445 | MR

[12] A. Letichevsky, J. Kapitonova, A. Letichevsky (Jr.), V. Volkov, S. Baranov, T. Weigert, “Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications”, Computer Networks: The International Journal of Computer and Telecommunications Networking, 49:5 (2005), 661–675 | Zbl

[13] H. Liang, J. Dingel, Z. Diskin, “A Comparative Survey of Scenario-Based to State-Based Model Synthesis Approaches”, Proceedings of SCESM 2006, ACM, NY, 2006, 5–12

[14] H. Muccini, “Detecting Implied Scenarios Analyzing Non-local Branching Choices”, FASE 2013, LNCS, 2621, 372–386 | Zbl

[15] O. R. Ribeiro, J. M. Fernandes, “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), 237–256

[16] A. Tanenbaum, Computers Networks, 4th Edition, Prentice Hall PTR, 2002 | Zbl

[17] N. Yang, H. Yu, H. Sun, Z. Qian, “Modeling UML sequence diagrams using extended Petri nets”, Telecommunication Systems, 51:2–3 (2012), 147–158 | DOI