Preview

Труды Института системного программирования РАН

Расширенный поиск

Prosega/CPN: расширение CPN Tools для автоматного анализа и верификации систем

https://doi.org/10.15514/ISPRAS-2018-30(4)-7

Аннотация

Верификация и анализ распределенных систем являются чрезвычайно важными задачами, особенно сейчас, когда многие компьютерные системы реализуют критически важные сервисы. Для моделирования и верификации систем полезно сочетать разные методы анализа. В частности, это позволяет применять тот формализм и ту технику анализа, которые лучше подходят для того или иного компонента системы. Комбинация из раскрашенных сетей Петри (CPN, Coloured Petri Nets) и конечных автоматов представляет собой успешную формальную методику моделирования и верификации распределенных систем. В связи с этим в данной статье рассматривается инструмент Prosega/CPN (Protocol Sequence Generator and Analyzer), расширение CPN Tools для поддержки автоматного анализа и верификации. Инструмент реализует несколько функций, таких как генерация минимизированного детерминированного конечного автомата из графа достижимости (occurrence graph) раскрашенной сети Петри, генерация языка и сопоставление конечных автоматов. Это решение поддерживается функцией Simulator Extensions, развитие которой обусловлено необходимостью интеграции раскрашенных сетей Петри с другими формализмами. Инструмент предназначен для поддержки формальной методологии верификации коммуникационных протоколов; однако он может использоваться для верификации других систем, анализ которых включает сравнение моделей на разных уровнях абстракции, например, бизнес-стратегий и бизнес-процессов. В статье приведен подробный пример, в котором инструмент Prosega/CPN используется для анализа части спецификации службы управления соединениями MAC IEEE 802.16.

Об авторах

Х. С. Карраскель
Римский университет Ла Сапиенца
Италия


А. Моралес
Центральный университет Венесуэлы
Венесуэла


М. Е. Виллаполь
Оклендский технологический университет
Новая Зеландия


Список литературы

1. T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, vol. 77, no. 4, April 1989, pp. 541-580

2. K. Jensen and L. M. Kristensen. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Berlin, Heidelberg: Springer-Verlag, 2009

3. CPN Tools - A tool for editing, simulating, and analyzing Coloured Petri Nets. Доступно по ссылке: http://www.cpntools.org/, дата обращения: 20.06.2018

4. M. Westergaard. CPN Tools 4: Multi-formalism and Extensibility. In Application and Theory of Petri Nets and Concurrency. Berlin, Heidelberg: Springer-Verlag, 2013, pp. 400-409

5. M. E. Villapol. Modelling and Analysis of the Resource Reservation Protocol Using Coloured Petri Nets. Ph.D. dissertation, University of South Australia, Australia, December 2003

6. S. Gordon, L. M. Kristensen, and J. Billington. Verification of a Revised WAP Wireless Transaction Protocol, In Application and Theory of Petri Nets and Concurrency. Berlin, Heidelberg: Springer-Verlag, 2002, pp. 182-202

7. B. Han. Formal Specification of the TCP Service and Verification of TCP Connection Management. Ph.D. dissertation, University of South Australia, Australia, April 2004

8. J. Billington, G. E. Gallasch, and B. Han. A Coloured Petri Net Approach to Protocol Verification. Berlin, Heidelberg: Springer-Verlag, 2004, pp. 210-290.

9. G. Gallasch and L. M. Kristensen. Comms/CPN: A Communication Infrastructure for External Communication with Design/CPN. In Proc. of the Third Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB-554, pages 75-91

10. M. Westergaard and K. B. Lassen. The BRITNeY Suite Animation Tool. In Applications and Theory of Petri Nets and Concurrency. Berlin, Heidelberg: Springer-Verlag, 2006, pp. 431-440

11. M. Westergaard. Access/CPN 2.0: A High-Level Interface to Coloured Petri Net Models. In Application and Theory of Petri Nets and Con- currency. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 328-337

12. AT&T Researchers - Inventing the Science Behind the Service. Доступно по ссылке: http: //www.research.att.com/evergreen/portfolio/, дата обращения: 20.06.2018

13. OpenFST Library. Доступно по ссылке: http://www.openfst.org/twiki/bin/view/FST/WebHome, дата обращения: 20.06.2018

14. M. Hulden. Foma: A Finite-state Compiler and Library. In Proceedings of the 12th Conference of the European Chapter of the Association for Computational Linguistics: Demonstrations Session. Stroudsburg, PA, USA: Association for Computational Linguistics, 2009, pp. 29-32

15. A. Almeida, M. Almeida, J. Alves, N. Moreira, and R. Reis. FAdo and GUItar: Tools for Automata Manipulation and Visualization. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2009, pp. 65-74

16. S. H. Rodger. JFLAP: An Interactive Formal Languages and Automata Package. USA: Jones and Bartlett Publishers, Inc., 2006

17. C. Ouyang and J. Billington. Formal Analysis of the Internet Open Trading Protocol. In Applying Formal Methods: Testing, Performance, and M/E-Commerce. Berlin, Heidelberg: Springer-Verlag, 2004, pp. 1-15

18. S. Barzegar, M. Davoudpour, M. R. Meybodi, A. Sadeghian, and M. Tirandazian. Traffic Signal Control with Adaptive Fuzzy Coloured Petri Net Based on Learning Automata. In Annual Meeting of the North American Fuzzy Information Processing Society, July 2010, pp. 1-8

19. N. Danapaquiame, E. Ilavarasan, N. Kumar, and S. K. Dwivedi. Ratification strategy for web service composition using CPN: A survey. In Proc. of the IEEE International Conference on Computational Intelligence and Computing Research, December 2013, pp. 1-4

20. J. Zhu, K. Zhang, and G. Zhang. Verifying Web Services Composition based on LTL and colored Petri Net. In Proc. of the 6th International Conference on Computer Science Education, August 2011, pp. 1127-1130

21. ISO/IEC. High-level Petri Nets - Part 1: Concepts, Definitions and Graphical Notation. Software and Systems Engineering, ISO/IEC FDIS 15909-1. Final Draft International.

22. W. A. Barrett and J. D. Couch. Compiler Construction: Theory and Practice. Chicago, Illinois: Science Research Associates Inc., 1979

23. M. Westergaard. CPN Tools 4 Extensions: Part 4: Advanced Communication and Debugging. Доступно по ссылке: https://westergaard.eu/2013/11/cpn-tools-4-extensions-part-4-advanced-communication-and-debugging/, November 2013, Blog entry/, дата обращения: 20.06.2018

24. C. Allauzen, M. Riley, J. Schalkwyk, W. Skut, and M. Mohri. OpenFst: A General and Efficient Weighted Finite-State Transducer Library. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2007, pp. 11-23.

25. Graphviz - Graph Visualization Software. Доступно по ссылке: http://www.graphviz.org//, дата обращения: 20.06.2018

26. J. C. Carrasquel. Java/PROSEGA: An extension in CPN Tools for generating languages accepted by FSA and minimized deterministic FSA from a state space. Central University of Venezuela, Caracas, Venezuela, Tech. Rep., October 2015.

27. IEEE 802.16 Working Group on Broadband Wireless Access Standards. IEEE Std. 802.16e-2005. Local and Metropolitan Area Network. Part 16: Air Interface for Fixed and Mobile Broadband Wireless Access Systems

28. A. V. Morales and M. E. Villapol. Towards Formal Specification of the Service in the IEEE 802.16 MAC Layer for Connection Management. In Proceedings of the 9th WSEAS International Conference on Computational Intelligence, Man-machine Systems and Cybernetics. World Scientific and Engineering Academy and Society (WSEAS), 2010, pp. 140-146

29. A. V. Morales and M. E. Villapol. Reviewing the Service Specification of the IEEE 802.16 MAC Layer Connection Management: A Formal Approach. CLEI Electronic Journal, vol. 16, August 2013, pp. 1- 12


Рецензия

Для цитирования:


Карраскель Х.С., Моралес А., Виллаполь М.Е. Prosega/CPN: расширение CPN Tools для автоматного анализа и верификации систем. Труды Института системного программирования РАН. 2018;30(4):107-128. https://doi.org/10.15514/ISPRAS-2018-30(4)-7

For citation:


Carrasquel J.C., Morales A., Villapol M.E. Prosega/CPN: An Extension of CPN Tools for Automata-based Analysis and System Verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):107-128. https://doi.org/10.15514/ISPRAS-2018-30(4)-7



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)