ИНСТРУМЕНТАЛЬНЫЕ СИСТЕМЫ, ПОДДЕРЖИВАЮЩИЕ СТОХАСТИЧЕСКИЕ СЕТЕВЫЕ МОДЕЛИ

Стохастические сети Петри - мощное средство моделирования параллельных недетерминиро­ванных систем с вероятностными характеристиками, применяемое в самых разных областях человеческой деятельности. Они сочетают наглядность графического представления с разви­тым математическим и алгоритмическим аппаратом анализа, позволяют изучать не только качественные, но и количественные свойства систем, такие как пропускная способность, на­дежность, время ожидания и т. и. Разработаны и продолжают появляться новые программные инструменты, поддерживающие создание, модификацию и анализ свойств моделей систем на основе различных вариантов стохастических сетей Петри. В данной работе рассматриваются несколько таких инструментов, доступных в сети Интернет и получивших признание пользова­телей, обсуждаются предоставляемые ими возможности и проводится их сравнение. Основная цель работы - облегчить исследователю и инженеру выбор наиболее подходящего инструмента моделирования и анализа для решения стоящей перед ним задачи.

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

1. Reisig W. Petri Nets: An Introduction. Vol. 4. Springer, 1985. (EATCS Monographs on Theoretical Computer Science). DOI: 10.1007/978-3-642-69968-9.
2. Boyer M., Roux O. On the Compared Expressiveness of Arc, Place and Transition Time Petri Nets // Fundamenta Informaticae. 2008. Jan. Vol. 88. P. 225-249.
3. Berthomieu B., Diaz M. Modeling and verification of time dependent systems using time Petri nets // IEEE Transactions on Software Engineering. 1991. Mar. Vol. 17, no. 3. P. 259-273. DOI: 10.1109/32.75415.
4. Molloy M. Performance Analysis Using Stochastic Petri Nets // IEEE Trans. Computers. 1982. Vol. 31, no. 9. P. 913-917. DOI: 10.1109/TC.1982.1676110.
5. Vicario E., Sassoli L., Carnevali L. Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems // IEEE Trans. Software Eng. 2009. Vol. 35, no. 5. P. 703-719. DOI: 10.1109/TSE.2009.36.
6. Wang J. Stochastic Timed Petri Nets and Stochastic Petri Nets // Timed Petri Nets: Theory and Application. Boston, MA : Springer US, 1998. P. 125-153. DOI: 10.1007/978-1-4615-5537-7,5.
7. Ajmone Marsan M. [et al.]. An introduction to generalized stochastic Petri nets // Microelectronics Reliability. 1991. Jan. Vol. 31, no. 4. P. 699-725. DOI: 10.1016/0026-2714(91)90010-5.
8. Ajmone Marsan M., Chiola G. On Petri nets with deterministic and exponentially distributed firing times // Advances in Petri Nets 1987, covers the 7th European Workshop on Applications and Theory of Petri Nets, Oxford, UK, June 1986. Vol. 266 / ed. by G. Rozenberg. Springer, 1986. P. 132-145. (Lecture Notes in Computer Science). DOI: 10.1007/3-540-18086-9,23.
9. Dugan J. [et al.]. Extended Stochastic Petri Nets: Applications and Analysis // Performance ’84, Proceedings of the Tenth International Symposium on Computer Performance Modelling, Measurement and Evaluation / ed. by E. Gelenbe. North-Holland, 1984. P. 507-519.
10. Ajmone Marsan M. [et al.]. The Effect of Execution Policies on the Semantics and Analysis of Stochastic Petri Nets // IEEE Trans. Software Eng. 1989. Vol. 15, no. 7. P. 832-846. DOI: 10.1109/32.29483.
11. German R., Lindemann C. Analysis of stochastic Petri nets by the method of supplementary variables // Performance Evaluation. 1994. May. Vol. 20, no. 1-3. P. 317-335. DOL 10.1016/0166- 5316(94)90020-5.
12. Тарасюк И. В. Стохастические сети Петри - формализм для моделирования и анализа производительности вычислительных процессов // Системная информатика. Новосибирск, 2004. С. 135-194.
13. German R. Performance analysis of communication systems : modelling with non- Markovian stochastic Petri nets. Wiley, 2000. P. 464.
14. Biagi M. [et al.]. Exploiting Non-deterministic Analysis in the Integration of Transient Solution Techniques for Markov Regenerative Processes // Quantitative Evaluation of Systems. Springer International Publishing, 2017. P. 20-35. DOL 10.1007/978-3-319-66335-7 2.
15. Martina S. [et al.]. Performance Evaluation of Fischer’s Protocol through SteadyState Analysis of Markov Regenerative Processes // 2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS). 09/2016. P. 355-360. DOL 10.1109/MASCOTS.2016.72.
16. Horva’th A. [et al.]. Transient analysis of non-Markovian models using stochastic state classes // Performance Evaluation. 2012. Vol. 69, no. 7/8. P. 315-335. DOL 10.1016/j.peva.2011.11.002.
17. Amparore Е. Stochastic Modelling and Evaluation Using GreatSPN // ACM SIGMETRICS Performance Evaluation Review. New York, NY, USA, 2022. June. Vol. 49, no. 4. P. 87-91. DOI: 10.1145/3543146.3543165.
18. Amparore E. [et al.]. 30 Years of GreatSPN // Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi on his 70th Birthday / ed. by L. Fiondella, A. Puliafito. Cham : Springer International Publishing, 2016. P. 227-254. DOI: 10.1007/978-3-319­30599-8-9.
19. K. J., Kristensen L. Coloured Petri Nets. Springer Berlin Heidelberg, 2009. DOI: 10.1007/b95112.
20. ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part 2: Transfer Format, International Standard ISO/IEC 15909, February 2011.
21. Kindler E. The Petri Net Markup Language and ISO/IEC 15909-2: Concepts, Status, and Future Directions // Tagungsband Entwurf komplexer Automatisierungssysteme EKA. 2006. P. 35-55.
22. Clarke E., Emerson E. Design and synthesis of synchronization skeletons using branching time temporal logic // Logics of Programs / ed. by D. Kozen. Springer Berlin Heidelberg, 1982. P. 52-71.
23. De’harbe D. A Tutorial Introduction to Symbolic Model Checking // Logic for Concurrency and Synchronisation / ed. by R. de Queiroz. Dordrecht : Springer Netherlands, 2003. P. 215-237. DOI: 10.1007/0-306-48088-3_5.
24. Beccuti M., Franceschinis G., Haddad S. Markov Decision Petri Net and Markov Decision Well- Formed Net Formalisms // Petri Nets and Other Models of Concurrency - ICATPN 2007 / ed. by J. Kleijn, A. Yakovlev. Springer Berlin Heidelberg, 2007. P. 43-62. DOI: 10.1007/978-3-540-73094-1-6.
25. Emerson E., Sistla A. Symmetry and model checking // Formal Methods in System Design. 1996. Vol. 9, no. 1. P. 105-131. DOL 10.1007/BF00625970.
26. Babar J. [et al.]. GreatSPN Enhanced with Decision Diagram Data Structures // Applications and Theory of Petri Nets / ed. by J. Lilius, W. Penczek. Springer Berlin Heidelberg, 2010. P. 308-317.
27. Chaki S., Gurfinkel A. BDD-Based Symbolic Model Checking // Handbook of Model Checking / ed. by E. Clarke [et al.]. Springer, 2018. P. 219-245. DOI: 10.1007/978-3-319-10575-8-8.
28. Rodriguez R., Bernardi S., Zimmermann A. An Evaluation Framework for Comparative Analysis of Generalized Stochastic Petri Net Simulation Techniques // IEEE Transactions on Systems, Man, and Cybernetics: Systems. 2020. Vol. 50. P. 2834-2844. DOL 10.1109/TSMC.2018.2837643.
29. Pernice S. [et al.]. Multiple Sclerosis Disease: A Computational Approach for Investigating Its Drug Interactions // Computational Intelligence Methods for Bioinformatics and Biostatistics / ed. by P. Cazzaniga [et al.]. Cham : Springer International Publishing, 2020. P. 299-308. DOI: 10.1007/978­3-030-63061-4 26.
30. Amparore E., Donatelli S., Landini E. Modelling and Evaluation of a Control Room Application // Application and Theory of Petri Nets and Concurrency / ed. by W. van der Aalst, E. Best. Cham : Springer International Publishing, 2017. P. 243-263.
31. Richard L. Performance Results for the CSMA/CD Protocol Using GreatSPN // Journal of Systems and Software. 1997. Vol. 37, no. 1. P. 75-90. DOI: 10.1016/S0164-1212(96)00041-6.
32. Amparore E., Donatelli S. GreatTeach: A Tool for Teaching (Stochastic) Petri Nets // Application and Theory of Petri Nets and Concurrency. Springer International Publishing, 2018. P. 416-425. DOL 10.1007/978-3-319-91268-4_24.
33. Castagno P. [et al.]. A computational framework for modeling and studying pertussis epidemiology and vaccination // BMC Bioinformatics. 2020. Vol. 21, no. 8. P. 344. DOL 10.1186/sl2859-020-03648-6.
34. The GreatSPN Framework. URL: https://github.com/greatspn/SOURCES Accessed: 01/12/2024.
35. Paolieri M. [et al.]. The ORIS Tool: Quantitative Evaluation of Non-Markovian Systems // IEEE Trans. Software Eng. 2021. Vol. 47, no. 6. P. 1211-1225. DOI: 10.1109/TSE.2019.2917202.
36. Carnevali L., Paolieri М., Vicario Е. The ORIS tool: app, library, and toolkit for quantitative evaluation of non-Markovian systems // ACM SIGMETRICS Performance Evaluation Review. 2022. Vol. 49, no. 4. P. 81-86. DOI: 10.1145/3543146.3543164.
37. Stewart W. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1995. DOI: 10.1515/9780691223384.
38. Carnevali L. [et al.]. Non-Markovian Performability Evaluation of ERTMS/ETCS Level 3 // Computer Performance Engineering - 12th European Workshop, EPEW 2015. Vol. 9272 / ed. by M. Beltran, W. Knottenbelt, J. Bradley. Cham : Springer, 2015. P. 47-62. (Lecture Notes in Computer Science). DOL 10.1007/978-3-319-23267-6_4.
39. Biagi M. [et al.]. Model-Based Quantitative Evaluation of Repair Procedures in Gas Distribution Networks // ACM Trans. Cyber Phys. Syst. 2019. Vol. 3, no. 2. 19:1-19:26. DOL 10.1145/3284037.
40. Carnevali L., Tarani F., Vicario F. Performability Evaluation of Water Distribution Systems During Maintenance Procedures // IEEE Trans. Syst. Man Cybern. Syst. 2020. Vol. 50, no. 5. P. 1704-1720. DOL 10.1109/TSMC.2017.2783188.
41. Carnevali L. [et al.]. Using the ORIS Tool and the SIRIO Library for Model- Driven Engineering of Quantitative Analytics // Computer Performance Engineering / ed. by K. Gilly, N. Thomas. Cham : Springer International Publishing, 2023. P. 200-215. DOL 10.1007/978-3-031-25049-1,13.
42. ORIS Tool. URL: http://www.oris-tool.org Accessed: 01/12/2024.
43. ORIS Tool: The Sirio Library. URL: https://github.com/oris-tool/sirio Accessed: 01/12/2024.
44. Heiner M. [et al.]. Snoopy - A Unifying Petri Net Tool // Application and Theory of Petri Nets. PETRI NETS 2012. Vol. 7347 / ed. by S. Haddad, L. Pomello. Springer Berlin Heidelberg, 2012. P. 398-407. (Lecture Notes in Computer Science). DOL 10.1007/978-3-642-31131-4_22.
45. David R., Alla H. Discrete, Continuous, and Hybrid Petri Nets. Springer Berlin Heidelberg, 2010. P. 550. DOL 10.1007/978-3-642-10669-9.
46. Liu F., Heiner M., Gilbert D. Fuzzy Petri nets for modelling of uncertain biological systems // Briefings in Bioinformatics. 2018. Dec. Vol. 21, no. 1. P. 198-210. DOL 10.1093/bib/bbyll8.
47. Fujita M., McGeer P., Yang J. Multi-Terminal Binary Decision Diagrams: An Efficient DataStructure for Matrix Representation // Form. Methods Syst. Des. USA, 1997. Apr. Vol. 10, no. 2/3. P. 149-169. DOL 10.1023/A: 1008647823331.
48. Hucka M. [et al.]. Systems Biology Markup Language (SBML) Level 2 Version 5: Structures and Facilities for Model Definitions // Journal of Integrative Bioinformatics. 2015. Vol. 12, no. 2. P. 731-901. DOL 10.2390/biecoll-jib-2015-271.
49. Heiner M., Schwarick M., Wegener J.-T. Charlie - An Extensible Petri Net Analysis Tool // Application and Theory of Petri Nets and Concurrency / ed. by R. Devillers, A. Valmari. Cham : Springer International Publishing, 2015. P. 200-211. DOL 10.1007/978-3-319-19488-2 10.
50. Heiner M., Rohr C., Schwarick M. MARCIE - Model Checking and Reachability Analysis Done Efficiently // Application and Theory of Petri Nets and Concurrency / ed. by J.-M. Colom, J. Desel. Springer Berlin Heidelberg, 2013. P. 389-399. DOI: 10.1007/978-3-642-38697-8-21.
51. Baier C. [et al.]. Model Checking Continuous-Time Markov Chains by Transient Analysis // Computer Aided Verification / ed. by E. Emerson, A. Sistla. Springer Berlin Heidelberg, 2000. P. 358-372.
52. Donaldson R., Gilbert D. A Model Checking Approach to the Parameter Estimation of Biochemical Pathways // Computational Methods in Systems Biology / ed. by M. Heiner, A. M. Uhrmacher. Springer Berlin Heidelberg, 2008. P. 269-287.
53. Chodak J., Heiner M. Spike - Reproducible Simulation Experiments with Configuration File Branching // Computational Methods in Systems Biology. Springer International Publishing, 2019. P. 315-321. DOL 10.1007/978-3-030-31304-3_19.
54. Gilbert D., Donaldson R. A Monte Carlo model checker for probabilistic LTL with numerical constraints : tech. rep. / Bioinformatics Research Centre, University of Glasgow. 01/2008.
55. Gilbert D. [et al.]. Spatial quorum sensing modelling using coloured hybrid Petri nets and simulative model checking // BMC Bioinformatics. 2019. Vol. 20, supplement 4. DOI: 10.1186/sl2859- 019-2690-z.
56. Herajy M. [et al.]. Snoopy’s hybrid simulator: a tool to construct and simulate hybrid biological models // BMC Systems Biology. 2017. July. Vol. 11, no. 1. DOI: 10.1186/sl2918-017-0449-6.
57. Zimmermann A. Modelling and Performance Evaluation with TimeNET 4.4 // Quantitative Evaluation of Systems - 14th International Conference, QEST 2017. Vol. 10503 / ed. by N. Bertrand, L. Bortolussi. Springer, 2017. P. 300-303. (Lecture Notes in Computer Science). DOI: 10.1007/978-3- 319-66335-7_19.
58. Selic B. Modeling And Analysis Of Realtime And Embedded Systems With Umi And Marte Developing Cyberphysical Systems. Elsevier Science & Technology, 2014. DOI: 10.1016/C2012-0-13536- 5.
59. Zimmermann A. [et al.]. Analysis of Safety-Critical Cloud Architectures with MultiTrajectory Simulation // 2022 Annual Reliability and Maintainability Symposium (RAMS). 01/2022. P. 1-7. DOI: 10.1109/RAMS51457.2022.9893923.
60. Fedorova A., Beliautsou V., Zimmermann A. Colored Petri Net Modelling and Evaluation of Drone Inspection Methods for Distribution Networks // Sensors. 2022. Vol. 22, no. 9. DOI: 10.3390/s22093418.
61. Dingle N., Knottenbelt W., Suto T. PIPE2: A Tool for the Performance Evaluation of Generalised Stochastic Petri Nets // SIGMETRICS Performance Evaluation Review ACM. New York, NY, USA, 2009. Mar. Vol. 36, no. 4. P. 34-39. DOI: 10.1145/1530873.1530881.
62. Platform Independent Petri Net Editor v4. URL: https://sourceforge.net/projects/pipe2 Accessed: 01/12/2024.
63. PIPE 5. URL: https://github.com/sarahtattersall/PIPE Accessed: 01/12/2024.