Применение раскрашенных сетей Петри для верификации распределенных систем, специфицированных MSC-диаграммами

Язык диаграмм последовательностей сообщений (MSC-диаграмм) является популярным сценарно-ориентированным языком спецификаций, который используется для описания взаимодействия компонент в распределенных системах. Однако методы и средства проверки корректности MSC-диаграмм недостаточно развиты. Эта статья описывает метод трансляции MSC-диаграмм в раскрашенные сети Петри (CPN). Метод используется для верификации свойств таких диаграмм. Рассматриваемое множество элементов диаграмм расширено элементами диаграмм взаимодействий стандарта UML и конструкциями композиционных MSC-диаграмм. Свойства результирующих CPN анализируются и верифицируются при помощи известной системы CPN Tools и верификатора CPN на основе системы SPIN. Применение данного метода продемонстрировано на примере.

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. С.А. Черненок, В.А. Непомнящий. Анализ MSC-диаграмм распределенных систем с помощью раскрашенных сетей Петри // Препринт 171, ИСИ СО РАН, Новосибирск, 2013. http://www.iis.nsk.su/files/preprints/171.pdf

19. С.А. Черненок, В.А. Непомнящий. Анализ и верификация MSC-диаграмм распределённых систем с помощью раскрашенных сетей Петри // Моделирование и анализ информационных систем, 2014 г., Т. 21, N 6, с. 94-106.

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. А.А. Стененко, В.А. Непомнящий. Верификация раскрашенных сетей Петри методом проверки моделей // Препринт 178, ИСИ СО РАН, Новосибирск, 2015. http://www.iis.nsk.su/files/preprints/178.pdf