Инструментальные системы, поддерживающие стохастические сетевые модели

Автор: Быстров А.В., Вирбицкайте И.Б., Ошевская Е.С.

Журнал: Проблемы информатики @problem-info

Рубрика: Прикладные информационные технологии

Статья в выпуске: 2 (63), 2024 года.

Бесплатный доступ

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

Еще

Стохастические сети петри, моделирование, анализ производительности, инструментальные системы

Короткий адрес: https://sciup.org/143183456

IDR: 143183456   |   УДК: 004.94+519.876.5   |   DOI: 10.24412/2073-0667-2024-2-32-57

Stochastic petri nets software tools

The behavior of a wide variety of systems, biochemical, transport, industrial, software, and so on, is inherently parallel, non-deterministic, and stochastic. The study and design of these systems requires the use of models that take into account all these aspects, as well as appropriate software tools. Stochastic Petri nets and their various extensions are successfully used as such models. They combine the clarity and intuitiveness of the graphical representation with well-developed mathematical and algorithmic apparatus of analysis. These models allow us to study not only qualitative but also quantitative properties of systems, such as bandwidth, reliability, waiting time, etc. Software tools that support the construction, modification and analysis of system models based on various variants of stochastic Petri nets have already been developed and continue to appear. This paper provides a detailed overview of several such multiplatfom software tools, namely, GreatSPN, ORIS, PetriNuts, TimeNet and PIPE2 that are available on the Internet, and got recognized by users. The introduction, informally, but with proper references to the literature, gives the basic concepts, defines the classes of Petri nets and terms used later. Then, for each of the software tools, its structure, features and peculiarities are considered. The tools are then compared in terms of their functional and performance analysis capabilities, and recommendations to users on how to use the tools depending on what type of stochastic models need to be investigated are discussed. The main purpose of the paper is to facilitate the researcher and engineer in selecting the most appropriate modeling and analysis tool for the task at hand.

Еще

Список литературы Инструментальные системы, поддерживающие стохастические сетевые модели

  • Reisig W. Petri Nets: An Introduction. V. 4. Springer, 1985. (EATCS Monographs on Theoretical Computer Science), DOI: 10.1007/978-3-642-69968-9.
  • Boyer M., Roux O. On the Compared Expressiveness of Arc, Place and Transition Time Petri Nets // Fundamenta Informaticae. 2008. Jan. V. 88. P. 225–249.
  • Berthomieu B., Diaz M. Modeling and verification of time dependent systems using time Petri nets // IEEE Transactions on Software Engineering. 1991. Mar. V. 17, N 3. P. 259–273. DOI: 10.1109/32.75415.
  • Molloy M. Performance Analysis Using Stochastic Petri Nets // IEEE Trans. Computers. 1982. V. 31, N 9. P. 913–917. DOI: 10.1109/TC.1982.1676110.
  • Vicario E., Sassoli L., Carnevali L. Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems // IEEE Trans. Software Eng. 2009. V. 35, N 5. P. 703–719. DOI: 10.1109/TSE.2009.36.
  • 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-l-4615-5537-7_5.
  • Ajmone Marsan M. et al. An introduction to generalized stochastic Petri nets // Microelectronics Reliability. 1991. Jan. V. 31, N 4. P. 699–725. DOI: 10.1016/0026-2714(91)90010-5.
  • Ajmone Marsan M., Chiola G. On Petri nets with deterministic and exponentially distributed Bring times // Advances in Petri Nets 1987, covers the 7th European Workshop on Applications and Theory of Petri Nets, Oxford, UK, June 1986. V. 266 / ed. by G. Rozenberg. Springer, 1986. P. 132–145. (Lecture Notes in Computer Science), DOI: 10.1007/3-540-18086-9_23.
  • 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.
  • Ajmone Marsan M. et al. The Effect of Execution Policies on the Semantics and Analysis of Stochastic Petri Nets // IEEE Trans. Software Eng. 1989. V. 15, N 7. P. 832–846. DOI: 10.1109/32.29483.
  • German R., Lindemann C. Analysis of stochastic Petri nets by the method of supplementary variables // Performance Evaluation. 1994. May. V. 20, N 1–3. P. 317–335. DOI: 10.1016/0166-5316(94)90020-5.
  • Тарасюк И. В. Стохастические сети Петри — формализм для моделирования и анализа производительности вычислительных процессов // Системная информатика. Новосибирск, 2004. С. 135–194.
  • German R. Performance analysis of communication systems — modelling with non- Markovian stochastic Petri nets: Modeling with Non-Markovian Stochastic Petri Nets. Wiley, 2000. P. 456.
  • 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. DOI: 10.1007/978-3-319-66335-7_2.
  • Martina S. et al. Performance Evaluation of Fischer’s Protocol through SteadyState Analysis of Markov Regenerative Processes // IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS). 09/2016. P. 355–360. DOI: 10.1109/MASCOTS.2016.72.
  • Horvath A. et al. Transient analysis of non-Markovian models using stochastic state classes // Performance Evaluation. 2012. V. 69, N 7/8. P. 315–335. DOI: 10.1016/j.peva.2011.11.002.
  • Amparore E. Stochastic Modelling and Evaluation Using GreatSPN // ACM- SIGMETRICS Performance Evaluation Review. New York, NY, USA, 2022. June. V. 49, N 4. P. 87–91. DOI: 10.1145/3543146.3543165.
  • Amparore E. et al. 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.
  • K. J., Kristensen L. Coloured Petri Nets. Springer Berlin Heidelberg, 2009. DOI: 10.1007/b95112.
  • ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part 2: Transfer Format, International Standard ISO/IEC 15909, February 2011.
  • Kindler E. The Petri Net Markup Language and ISO/IEC 15909-2: Concepts, Status, and Future Directions // Tagungsband Entwurf komplcxcr Automatisierungssysteme EKA. 2006. P. 35–55.
  • 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.
  • Deharbe 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.
  • 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.
  • Emerson E., Sistla A. Symmetry and model checking // Formal Methods in System Design. 1996. V. 9, N 1. P. 105–131. DOI: 10.1007/BF00625970.
  • Babar J. et al. GrcatSPN 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.
  • 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.
  • R. R., S. B., Zimmermann A. An Evaluation Framework for Comparative Analysis of Generalized Stochastic Petri Net Simulation Techniques // IEEE Transactions on Systems, Man, and Cybernetics: Systems. 2020. V. 50. P. 2834–2844. DOI: 10.1109/TSMC.2018.2837643.
  • 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.
  • 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.
  • Richard L. Performance Results for the CSMA/CD Protocol Using GrcatSPN // Journal of Systems and Software. 1997. V. 37, N 1. P. 75–90. DOI: 10.1016/S0164-1212(96)00041-6.
  • Amparore E., Donatelli S. GreatTeach: A Tool for Teaching (Stochastic) Petri Nets // Application nd Theory of Petri Nets and Concurrency. Springer International Publishing, 2018. P. 416–425. DOI: 10.1007/978-3-319-91268-4_24.
  • Castagno P. et al. A computational framework for modeling and studying pertussis epidemiology and vaccination // BMC Bioinformatics. 2020. V. 21, N 8. P. 344. DOI: 10.1186/S12859-020-03648-6.
  • The GrcatSPN Framework. [El. Res.]: https://github.com/greatspn/SOURCES. Accessed: 2024-03-15.
  • Paolieri M. et al. The ORIS Tool: Quantitative Evaluation of Non-Markovian Systems // IEEE Trans. Software Eng. 2021. V. 47, N 6. P. 1211–1225. DOI: 10.1109/TSE.2019.2917202.
  • Carnevali L., Paolieri M., Vicario E. The ORIS tool: app, library, and toolkit for quantitative evaluation of non-Markovian systems // ACM SIGMETRICS Performance Evaluation Review. 2022. V. 49, N 4. P. 81–86. DOI: 10.1145/3543146.3543164.
  • Stewart W. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1995. DOI: 10.1515/9780691223384.
  • Carnevali L. et al. Non-Markovian Performability Evaluation of ERTMS/ETCS Level 3 // Computer Performance Engineering - 12th European Workshop, EPEW 2015. V. 9272 / ed. by M. Beltran, W. Knottenbelt, J. Bradley. Cham: Springer, 2015. P. 47–62. (Lecture Notes in Computer Science), DOI: 10.1007/978-3-319-23267-6_4.
  • Biagi M. et al. Model-Based Quantitative Evaluation of Repair Procedures in Gas Distribution Networks // ACM Trans. Cyber Phys. Syst. 2019. V. 3, N 2. 19:1–19:26. DOI: 10.1145/3284037.
  • Carnevali L., Tarani F., Vicario F. Performability Evaluation of Water Distribution Systems During Maintenance Procedures // IEEE Trans. Syst. Man Cybern. Syst. 2020. V. 50, N 5. P. 1704–1720. DOI: 10.1109/TSMC.2017.2783188.
  • Carnevali L. et al. Using the ORIS Tool and the SIRIO Library for Model- Driven Engineering of Quantitative Analytics // Computer Performance Engineering / ed. byK. Gilly, N. Thomas. Cham: Springer International Publishing, 2023. P. 200–215. DOI: 10.1007/978-3-031-25049-l_13.
  • ORIS Tool. [El. Res.]: http://www.oris-tool.org. Accessed: 2024-03-15.
  • ORIS Tool: The Sirio Library. [El. Res.]: https://github.com/oris-tool/sirio. Accessed: 2024-03-15.
  • Heiner M. et al. Snoopy — A Unifying Petri Net Tool // Application and Theory of Petri Nets. PETRI NETS 2012. V. 7347 / ed. by S. Haddad, L. Pomello. Springer Berlin Heidelberg, 2012. P. 398–407. (Lecture Notes in Computer Science), DOI: 10.1007/978-3-642-31131-4_22.
  • David R., Alla H. Discrete, Continuous, and Hybrid Petri Nets. Springer Berlin Heidelberg, 2010. P. 550. DOI: 10.1007/978-3-642-10669-9.
  • Liu F., Heiner M., Gilbert D. Fuzzy Petri nets for modelling of uncertain biological systems // Briefings in Bioinformatics. 2018. Dec. V. 21, N 1. P. 198–210. DOI: 10.1093/bib/bbyll8.
  • Fujita M., McGeer P., Yang J. Multi-Terminal Binary Decision Diagrams: An Efficient DataStructure for Matrix Representation // Form. Methods Syst. Des. USA, 1997. Apr. V. 10, N 2/3. P. 149–169. DOI: 10.1023/A: 1008647823331.
  • Hucka M. et al. Systems Biology Markup Language (SBML) Level 2 Version 5: Structures and Facilities for Model Definitions // Journal of Integrative Bioinformatics. 2015. V. 12. N 2. P. 731–901. DOI: 10.2390/biecoll-jib-2015-271.
  • 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. DOI: 10.1007/978-3-319-19488-2_10.
  • Heiner M., Rohr C., Schwarick M. MARGIE — 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.
  • 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.
  • 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.
  • Chodak J., Heiner M. Spike — Reproducible Simulation Experiments with Configuration File Branching // Computational Methods in Systems Biology. Springer International Publishing, 2019. P. 315–321. DOI: 10.1007/978-3-030-31304-3_19.
  • 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.
  • Gilbert D. et al. Spatial quorum sensing modelling using coloured hybrid Petri nets and simulative model checking // BMC Bioinformatics. 2019. V. 20, supplement 4. DOI: 10.1186/sl2859-019-2690-z.
  • Hcrajy M. et al. Snoopy’s hybrid simulator: a tool to construct and simulate hybrid biological models // BMC Systems Biology. 2017. July. V. 11, N 1. DOI: 10.1186/S12918-017-0449-6.
  • Zimmermann A. Modelling and Performance Evaluation with TimeNET 4.4 // Quantitative Evaluation of Systems - 14th International Conference, QEST 2017. V. 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.
  • Selic B. Modeling And Analysis Of Realtime And Embedded Systems With Uml And Marte Developing Cyberphysical Systems. Elsevier Science & Technology, 2014. DOI: 10.1016/C2012-0-13536-5.
  • Zimmermann A. et al. Analysis of Safety-Critical Cloud Architectures with MultiTrajectory Simulation // Annual Reliability and Maintainability Symposium (RAMS). 01/2022. P. 1–7. DOI: 10.1109/RAMS51457.2022.9893923.
  • Fedorova A., Beliautsou V., Zimmermann A. Colored Petri Net Modelling and Evaluation of Drone Inspection Methods for Distribution Networks // Sensors. 2022. V. 22, N 9. DOI: 10.3390/s22093418.
  • 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. V. 36, N 4. P. 34–39. DOI: 10.1145/1530873.1530881.
  • Platform Independent Petri Net Editor v4. [El. Res.]: https://sourceforge.net/projects/ pipe2. Accessed: 2024-03-15.
  • PIPE 5. [El. Res.]: https://github.com/sarahtattersall/PIPE. Accessed: 2024-03-15.
Еще