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

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

1. ITU-T Recommendation Z.120 (02/2011): Message Sequence Charts (MSC), 2011.

2. Unified Modeling Language (UML) 2.5. Object Management Group, 2013. (http://www.omg.org/spec/UML/2.5/Beta2/)

3. Genest B. Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs. TACAS 2005, LNCS 3440, 2005. P. 429-444.

4. Genest B., Muscholl A., Peled D. Message Sequence Charts. Lectures on Concurrency and Petri Nets, LNCS 3098, 2003. P. 537-558.

5. Rajeev Alur, Holzmann G.J., Peled D. An Analyzer for Message Sequence Charts. TACAS 96, LNCS 1055, 1996. P. 35-48.

6. UBET (MSC/POGA) toolset - http://cm.bell-labs.com/cm/cs/what/ubet/index.html

7. Cinderella MSC computer tool - http://www.cinderella.dk/msc.htm

8. IBM Rational Tau system - www.ibm.com/software/products/en/ratitau

9. Gaudin E., Brunel E. Property Verification with MSC. SDL 2013, LNCS 7916, 2013. P. 19-35.

10. Fernandes J.M., Tjell S., Jorgensen J.B., Ribeiro O. Designing Tool Support for Translating Use Cases and UML 2.0 Sequence Diagrams into a Coloured Petri Net. SCESM '07: Proc. of the Sixth International Workshop on Scenarios and State Machines, Washington, DC, USA, 2007. P. 2.

11. Yang N., Yu H., Sun H., Qian Z. Modeling UML sequence diagrams using extended Petri nets, Telecommunication Systems, Springer, 2012. V. 51, N. 2-3, P. 147-158.

12. Eichner C., Fleischhack H., Meyer R., Schrimpf U., Stehno S. Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets. SDL-Forum 2005, LNCS 3530, 2005. P. 133-148.

13. Lima V., Talhi C., Mouheb D., Debbabi M., Wang L., Pourzandi M. Formal verification and validation of UML 2.0 Sequence Diagrams using source and destination of messages. Electron. Notes Theor. Comput. Sci., 2009. V. 254, P. 143-160.

14. Shen H., Robinson M., Niu J. Model Checking Combined Fragments of Sequence Diagrams. Software and Data Technologies, Springer, 2013. V. 411, P. 96-111.

15. Holzmann G. The Spin model checker: primer and reference manual. Addison Wesley, 2003. 608 p.

16. Jensen K., Kristensen L.M. Coloured Petri Nets: Modeling and Validation of Concurrent Systems, Springer, 2009. 384 p.

17. Micskei Z., Waeselynck H. The many meanings of UML 2 Sequence Diagrams: a survey. Software and Systems Modeling, Springer, 2011. V. 10, N. 4, P. 489-514.

18. Chernenok S.A., Nepomniaschy V.A. Analysis of Message Sequence Charts of Distributed Systems Using Coloured Petri Nets, Preprint 171, Institute of Informatics Systems, Novosibirsk, 2013 (in Russian). http://www.iis.nsk.su/files/preprints/171.pdf

19. Chernenok S.A., Nepomniaschy V.A. Analysis and Verification of Message Sequence Charts of Distributed Systems with the Help of Coloured Petri Nets. Modeling and Analysis of Information Systems, 2014. V. 21, N. 6, P. 94-106 (in Russian).

20. Haugen O. Comparing UML 2.0 Interactions and MSC-2000. 4th International SDL and MSC Workshop, LNCS 3319, 2005. P. 65-79.

21. Abdallah R., Gotlieb A., Helouet L., Jard C. Scenario Realizability with Constraint Optimization. FASE 2013, LNCS 7793, 2013. P. 194-209.

22. Tel G. Introduction to distributed algorithms. Cambridge University Press New York, USA, 2000. 612 p.

23. Chernenok S. A. Examples of Analysis and Verification of Message Sequence Charts. Appendix, 2015. (http://bitbucket.org/chernenok/msc-verification)

24. Stenenko A.A., Nepomniaschy V.A. Model Checking Approach to Verification of Coloured Petri Nets, Preprint 178, Institute of Informatics Systems SB RAS, Novosibirsk, 2015 (in Russian). http://www.iis.nsk.su/files/preprints/178.pdf